H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 3.478 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(m,_)→m

is transformed to

m0 (m,_) = m

The following Lambda expression

\(_,r)→r

is transformed to

r0 (_,r) = r

The following Lambda expression

\(q,_)→q

is transformed to

q1 (q,_) = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

frac@(Double vy vz)

is replaced by the following term

Double vy vz

The bind variable of the following binding Pattern

frac@(Float ww wx)

is replaced by the following term

Float ww wx

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

toEnum 0 = False

toEnum 1 = True

is transformed to

toEnum xz = toEnum3 xz

toEnum xy = toEnum1 xy

toEnum0 True xy = True

toEnum1 xy = toEnum0 (xy == 1) xy

toEnum2 True xz = False

toEnum2 yu yv = toEnum1 yv

toEnum3 xz = toEnum2 (xz == 0) xz

toEnum3 yw = toEnum1 yw

The following Function with conditions

toEnum 0 = ()

is transformed to

toEnum yx = toEnum5 yx

toEnum4 True yx = ()

toEnum5 yx = toEnum4 (yx == 0) yx

The following Function with conditions

toEnum 0 = LT

toEnum 1 = EQ

toEnum 2 = GT

is transformed to

toEnum zx = toEnum11 zx

toEnum yz = toEnum9 yz

toEnum yy = toEnum7 yy

toEnum6 True yy = GT

toEnum7 yy = toEnum6 (yy == 2) yy

toEnum8 True yz = EQ

toEnum8 zu zv = toEnum7 zv

toEnum9 yz = toEnum8 (yz == 1) yz

toEnum9 zw = toEnum7 zw

toEnum10 True zx = LT

toEnum10 zy zz = toEnum9 zz

toEnum11 zx = toEnum10 (zx == 0) zx

toEnum11 vuu = toEnum9 vuu

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

m

where

m = m0 vu6

m0 (m,vv) = m

vu6 = properFraction x

are unpacked to the following functions on top level

truncateM vuv = truncateM0 vuv (truncateVu6 vuv)

truncateVu6 vuv = properFraction vuv

truncateM0 vuv (m,vv) = m

The bindings of the following Let/Where expression

(fromIntegral q,r :% y)

where

q = q1 vu30

q1 (q,xv) = q

r = r0 vu30

r0 (xw,r) = r

vu30 = quotRem x y

are unpacked to the following functions on top level

properFractionR vuw vux = properFractionR0 vuw vux (properFractionVu30 vuw vux)

properFractionQ1 vuw vux (q,xv) = q

properFractionQ vuw vux = properFractionQ1 vuw vux (properFractionVu30 vuw vux)

properFractionR0 vuw vux (xw,r) = r

properFractionVu30 vuw vux = quotRem vuw vux

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

mainModule Main

(pred :: Enum a => a -> a)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="pred\n  Enum a",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="pred vuy3\n  Enum a",fontsize=16,color="blue",shape="box"];2541[label="pred :: Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];3 -> 2541[label="",style="solid", color="blue", weight=9];
2541 -> 4[label="",style="solid", color="blue", weight=3];
2542[label="pred :: (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];3 -> 2542[label="",style="solid", color="blue", weight=9];
2542 -> 5[label="",style="solid", color="blue", weight=3];
2543[label="pred :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];3 -> 2543[label="",style="solid", color="blue", weight=9];
2543 -> 6[label="",style="solid", color="blue", weight=3];
2544[label="pred :: Double -> Double",fontsize=10,color="white",style="solid",shape="box"];3 -> 2544[label="",style="solid", color="blue", weight=9];
2544 -> 7[label="",style="solid", color="blue", weight=3];
2545[label="pred :: () -> ()",fontsize=10,color="white",style="solid",shape="box"];3 -> 2545[label="",style="solid", color="blue", weight=9];
2545 -> 8[label="",style="solid", color="blue", weight=3];
2546[label="pred :: Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];3 -> 2546[label="",style="solid", color="blue", weight=9];
2546 -> 9[label="",style="solid", color="blue", weight=3];
2547[label="pred :: Char -> Char",fontsize=10,color="white",style="solid",shape="box"];3 -> 2547[label="",style="solid", color="blue", weight=9];
2547 -> 10[label="",style="solid", color="blue", weight=3];
2548[label="pred :: Float -> Float",fontsize=10,color="white",style="solid",shape="box"];3 -> 2548[label="",style="solid", color="blue", weight=9];
2548 -> 11[label="",style="solid", color="blue", weight=3];
2549[label="pred :: Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];3 -> 2549[label="",style="solid", color="blue", weight=9];
2549 -> 12[label="",style="solid", color="blue", weight=3];
4[label="pred vuy3",fontsize=16,color="burlywood",shape="box"];2550[label="vuy3/Integer vuy30",fontsize=10,color="white",style="solid",shape="box"];4 -> 2550[label="",style="solid", color="burlywood", weight=9];
2550 -> 13[label="",style="solid", color="burlywood", weight=3];
5[label="pred vuy3\n  Integral a",fontsize=16,color="black",shape="box"];5 -> 14[label="",style="solid", color="black", weight=3];
6[label="pred vuy3",fontsize=16,color="burlywood",shape="triangle"];2551[label="vuy3/Pos vuy30",fontsize=10,color="white",style="solid",shape="box"];6 -> 2551[label="",style="solid", color="burlywood", weight=9];
2551 -> 15[label="",style="solid", color="burlywood", weight=3];
2552[label="vuy3/Neg vuy30",fontsize=10,color="white",style="solid",shape="box"];6 -> 2552[label="",style="solid", color="burlywood", weight=9];
2552 -> 16[label="",style="solid", color="burlywood", weight=3];
7[label="pred vuy3",fontsize=16,color="black",shape="box"];7 -> 17[label="",style="solid", color="black", weight=3];
8[label="pred vuy3",fontsize=16,color="black",shape="box"];8 -> 18[label="",style="solid", color="black", weight=3];
9[label="pred vuy3",fontsize=16,color="black",shape="box"];9 -> 19[label="",style="solid", color="black", weight=3];
10[label="pred vuy3",fontsize=16,color="black",shape="box"];10 -> 20[label="",style="solid", color="black", weight=3];
11[label="pred vuy3",fontsize=16,color="black",shape="box"];11 -> 21[label="",style="solid", color="black", weight=3];
12[label="pred vuy3",fontsize=16,color="black",shape="box"];12 -> 22[label="",style="solid", color="black", weight=3];
13[label="pred (Integer vuy30)",fontsize=16,color="black",shape="box"];13 -> 23[label="",style="solid", color="black", weight=3];
14[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum\n  Integral a",fontsize=16,color="black",shape="box"];14 -> 24[label="",style="solid", color="black", weight=3];
15[label="pred (Pos vuy30)",fontsize=16,color="burlywood",shape="box"];2553[label="vuy30/Succ vuy300",fontsize=10,color="white",style="solid",shape="box"];15 -> 2553[label="",style="solid", color="burlywood", weight=9];
2553 -> 25[label="",style="solid", color="burlywood", weight=3];
2554[label="vuy30/Zero",fontsize=10,color="white",style="solid",shape="box"];15 -> 2554[label="",style="solid", color="burlywood", weight=9];
2554 -> 26[label="",style="solid", color="burlywood", weight=3];
16[label="pred (Neg vuy30)",fontsize=16,color="burlywood",shape="box"];2555[label="vuy30/Succ vuy300",fontsize=10,color="white",style="solid",shape="box"];16 -> 2555[label="",style="solid", color="burlywood", weight=9];
2555 -> 27[label="",style="solid", color="burlywood", weight=3];
2556[label="vuy30/Zero",fontsize=10,color="white",style="solid",shape="box"];16 -> 2556[label="",style="solid", color="burlywood", weight=9];
2556 -> 28[label="",style="solid", color="burlywood", weight=3];
17[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];17 -> 29[label="",style="solid", color="black", weight=3];
18[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];18 -> 30[label="",style="solid", color="black", weight=3];
19[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];19 -> 31[label="",style="solid", color="black", weight=3];
20[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];20 -> 32[label="",style="solid", color="black", weight=3];
21[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];21 -> 33[label="",style="solid", color="black", weight=3];
22[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];22 -> 34[label="",style="solid", color="black", weight=3];
23[label="Integer (pred vuy30)",fontsize=16,color="green",shape="box"];23 -> 35[label="",style="dashed", color="green", weight=3];
24[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)\n  Integral a",fontsize=16,color="black",shape="box"];24 -> 36[label="",style="solid", color="black", weight=3];
25[label="pred (Pos (Succ vuy300))",fontsize=16,color="black",shape="box"];25 -> 37[label="",style="solid", color="black", weight=3];
26[label="pred (Pos Zero)",fontsize=16,color="black",shape="box"];26 -> 38[label="",style="solid", color="black", weight=3];
27[label="pred (Neg (Succ vuy300))",fontsize=16,color="black",shape="box"];27 -> 39[label="",style="solid", color="black", weight=3];
28[label="pred (Neg Zero)",fontsize=16,color="black",shape="box"];28 -> 40[label="",style="solid", color="black", weight=3];
29[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];29 -> 41[label="",style="solid", color="black", weight=3];
30[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];30 -> 42[label="",style="solid", color="black", weight=3];
31[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];31 -> 43[label="",style="solid", color="black", weight=3];
32[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];32 -> 44[label="",style="solid", color="black", weight=3];
33[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];33 -> 45[label="",style="solid", color="black", weight=3];
34[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];34 -> 46[label="",style="solid", color="black", weight=3];
35 -> 6[label="",style="dashed", color="red", weight=0];
35[label="pred vuy30",fontsize=16,color="magenta"];35 -> 47[label="",style="dashed", color="magenta", weight=3];
36[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum)\n  Integral a",fontsize=16,color="black",shape="box"];36 -> 48[label="",style="solid", color="black", weight=3];
37[label="Pos vuy300",fontsize=16,color="green",shape="box"];38[label="Neg (Succ Zero)",fontsize=16,color="green",shape="box"];39[label="Neg (Succ (Succ vuy300))",fontsize=16,color="green",shape="box"];40[label="Neg (Succ Zero)",fontsize=16,color="green",shape="box"];41[label="primIntToDouble ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];41 -> 49[label="",style="solid", color="black", weight=3];
42[label="toEnum5 ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];42 -> 50[label="",style="solid", color="black", weight=3];
43[label="toEnum3 ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];43 -> 51[label="",style="solid", color="black", weight=3];
44[label="primIntToChar ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];44 -> 52[label="",style="solid", color="black", weight=3];
45[label="primIntToFloat ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];45 -> 53[label="",style="solid", color="black", weight=3];
46[label="toEnum11 ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];46 -> 54[label="",style="solid", color="black", weight=3];
47[label="vuy30",fontsize=16,color="green",shape="box"];48[label="intToRatio ((subtract (Pos (Succ Zero))) . fromEnum)\n  Integral a",fontsize=16,color="black",shape="box"];48 -> 55[label="",style="solid", color="black", weight=3];
49[label="Double ((subtract (Pos (Succ Zero))) . fromEnum) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];49 -> 56[label="",style="dashed", color="green", weight=3];
50[label="toEnum4 ((subtract (Pos (Succ Zero))) . fromEnum == Pos Zero) ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];50 -> 57[label="",style="solid", color="black", weight=3];
51[label="toEnum2 ((subtract (Pos (Succ Zero))) . fromEnum == Pos Zero) ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];51 -> 58[label="",style="solid", color="black", weight=3];
52[label="primIntToChar (subtract (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];52 -> 59[label="",style="solid", color="black", weight=3];
53[label="Float ((subtract (Pos (Succ Zero))) . fromEnum) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];53 -> 60[label="",style="dashed", color="green", weight=3];
54[label="toEnum10 ((subtract (Pos (Succ Zero))) . fromEnum == Pos Zero) ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];54 -> 61[label="",style="solid", color="black", weight=3];
55[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum) :% fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="green",shape="box"];55 -> 62[label="",style="dashed", color="green", weight=3];
55 -> 63[label="",style="dashed", color="green", weight=3];
56[label="(subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];56 -> 64[label="",style="solid", color="black", weight=3];
57[label="toEnum4 (primEqInt ((subtract (Pos (Succ Zero))) . fromEnum) (Pos Zero)) ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];57 -> 65[label="",style="solid", color="black", weight=3];
58[label="toEnum2 (primEqInt ((subtract (Pos (Succ Zero))) . fromEnum) (Pos Zero)) ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];58 -> 66[label="",style="solid", color="black", weight=3];
59[label="primIntToChar (flip (-) (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];59 -> 67[label="",style="solid", color="black", weight=3];
60[label="(subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];60 -> 68[label="",style="solid", color="black", weight=3];
61[label="toEnum10 (primEqInt ((subtract (Pos (Succ Zero))) . fromEnum) (Pos Zero)) ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];61 -> 69[label="",style="solid", color="black", weight=3];
62[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum)\n  Integral a",fontsize=16,color="blue",shape="box"];2558[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];62 -> 2558[label="",style="solid", color="blue", weight=9];
2558 -> 70[label="",style="solid", color="blue", weight=3];
2559[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];62 -> 2559[label="",style="solid", color="blue", weight=9];
2559 -> 71[label="",style="solid", color="blue", weight=3];
63[label="fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];2560[label="fromInt :: -> Int Int",fontsize=10,color="white",style="solid",shape="box"];63 -> 2560[label="",style="solid", color="blue", weight=9];
2560 -> 72[label="",style="solid", color="blue", weight=3];
2561[label="fromInt :: -> Int Integer",fontsize=10,color="white",style="solid",shape="box"];63 -> 2561[label="",style="solid", color="blue", weight=9];
2561 -> 73[label="",style="solid", color="blue", weight=3];
64[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];64 -> 74[label="",style="solid", color="black", weight=3];
65[label="toEnum4 (primEqInt (subtract (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (subtract (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];65 -> 75[label="",style="solid", color="black", weight=3];
66[label="toEnum2 (primEqInt (subtract (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (subtract (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];66 -> 76[label="",style="solid", color="black", weight=3];
67[label="primIntToChar ((-) fromEnum vuy3 Pos (Succ Zero))",fontsize=16,color="black",shape="box"];67 -> 77[label="",style="solid", color="black", weight=3];
68[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];68 -> 78[label="",style="solid", color="black", weight=3];
69[label="toEnum10 (primEqInt (subtract (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (subtract (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];69 -> 79[label="",style="solid", color="black", weight=3];
70[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];70 -> 80[label="",style="solid", color="black", weight=3];
71[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="black",shape="box"];71 -> 81[label="",style="solid", color="black", weight=3];
72[label="fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];72 -> 82[label="",style="solid", color="black", weight=3];
73[label="fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];73 -> 83[label="",style="solid", color="black", weight=3];
74[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];74 -> 84[label="",style="solid", color="black", weight=3];
75[label="toEnum4 (primEqInt (flip (-) (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (flip (-) (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];75 -> 85[label="",style="solid", color="black", weight=3];
76[label="toEnum2 (primEqInt (flip (-) (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (flip (-) (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];76 -> 86[label="",style="solid", color="black", weight=3];
77[label="primIntToChar (primMinusInt (fromEnum vuy3) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];77 -> 87[label="",style="solid", color="black", weight=3];
78[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];78 -> 88[label="",style="solid", color="black", weight=3];
79[label="toEnum10 (primEqInt (flip (-) (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (flip (-) (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];79 -> 89[label="",style="solid", color="black", weight=3];
80[label="(subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];80 -> 90[label="",style="solid", color="black", weight=3];
81[label="Integer ((subtract (Pos (Succ Zero))) . fromEnum)",fontsize=16,color="green",shape="box"];81 -> 91[label="",style="dashed", color="green", weight=3];
82[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];83[label="Integer (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];84[label="(-) fromEnum vuy3 Pos (Succ Zero)",fontsize=16,color="black",shape="box"];84 -> 92[label="",style="solid", color="black", weight=3];
85[label="toEnum4 (primEqInt ((-) fromEnum vuy3 Pos (Succ Zero)) (Pos Zero)) ((-) fromEnum vuy3 Pos (Succ Zero))",fontsize=16,color="black",shape="box"];85 -> 93[label="",style="solid", color="black", weight=3];
86[label="toEnum2 (primEqInt ((-) fromEnum vuy3 Pos (Succ Zero)) (Pos Zero)) ((-) fromEnum vuy3 Pos (Succ Zero))",fontsize=16,color="black",shape="box"];86 -> 94[label="",style="solid", color="black", weight=3];
87[label="primIntToChar (primMinusInt (primCharToInt vuy3) (Pos (Succ Zero)))",fontsize=16,color="burlywood",shape="box"];2562[label="vuy3/Char vuy30",fontsize=10,color="white",style="solid",shape="box"];87 -> 2562[label="",style="solid", color="burlywood", weight=9];
2562 -> 95[label="",style="solid", color="burlywood", weight=3];
88[label="(-) fromEnum vuy3 Pos (Succ Zero)",fontsize=16,color="black",shape="box"];88 -> 96[label="",style="solid", color="black", weight=3];
89[label="toEnum10 (primEqInt ((-) fromEnum vuy3 Pos (Succ Zero)) (Pos Zero)) ((-) fromEnum vuy3 Pos (Succ Zero))",fontsize=16,color="black",shape="box"];89 -> 97[label="",style="solid", color="black", weight=3];
90[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];90 -> 98[label="",style="solid", color="black", weight=3];
91[label="(subtract (Pos (Succ Zero))) . fromEnum",fontsize=16,color="black",shape="box"];91 -> 99[label="",style="solid", color="black", weight=3];
92[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];92 -> 100[label="",style="solid", color="black", weight=3];
93[label="toEnum4 (primEqInt (primMinusInt (fromEnum vuy3) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum vuy3) (Pos (Succ Zero)))",fontsize=16,color="burlywood",shape="box"];2563[label="vuy3/()",fontsize=10,color="white",style="solid",shape="box"];93 -> 2563[label="",style="solid", color="burlywood", weight=9];
2563 -> 101[label="",style="solid", color="burlywood", weight=3];
94[label="toEnum2 (primEqInt (primMinusInt (fromEnum vuy3) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum vuy3) (Pos (Succ Zero)))",fontsize=16,color="burlywood",shape="box"];2564[label="vuy3/False",fontsize=10,color="white",style="solid",shape="box"];94 -> 2564[label="",style="solid", color="burlywood", weight=9];
2564 -> 102[label="",style="solid", color="burlywood", weight=3];
2565[label="vuy3/True",fontsize=10,color="white",style="solid",shape="box"];94 -> 2565[label="",style="solid", color="burlywood", weight=9];
2565 -> 103[label="",style="solid", color="burlywood", weight=3];
95[label="primIntToChar (primMinusInt (primCharToInt (Char vuy30)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];95 -> 104[label="",style="solid", color="black", weight=3];
96[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];96 -> 105[label="",style="solid", color="black", weight=3];
97[label="toEnum10 (primEqInt (primMinusInt (fromEnum vuy3) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum vuy3) (Pos (Succ Zero)))",fontsize=16,color="burlywood",shape="box"];2566[label="vuy3/LT",fontsize=10,color="white",style="solid",shape="box"];97 -> 2566[label="",style="solid", color="burlywood", weight=9];
2566 -> 106[label="",style="solid", color="burlywood", weight=3];
2567[label="vuy3/EQ",fontsize=10,color="white",style="solid",shape="box"];97 -> 2567[label="",style="solid", color="burlywood", weight=9];
2567 -> 107[label="",style="solid", color="burlywood", weight=3];
2568[label="vuy3/GT",fontsize=10,color="white",style="solid",shape="box"];97 -> 2568[label="",style="solid", color="burlywood", weight=9];
2568 -> 108[label="",style="solid", color="burlywood", weight=3];
98[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];98 -> 109[label="",style="solid", color="black", weight=3];
99[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];99 -> 110[label="",style="solid", color="black", weight=3];
100[label="primMinusInt (truncate vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];100 -> 111[label="",style="solid", color="black", weight=3];
101[label="toEnum4 (primEqInt (primMinusInt (fromEnum ()) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum ()) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];101 -> 112[label="",style="solid", color="black", weight=3];
102[label="toEnum2 (primEqInt (primMinusInt (fromEnum False) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum False) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];102 -> 113[label="",style="solid", color="black", weight=3];
103[label="toEnum2 (primEqInt (primMinusInt (fromEnum True) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum True) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];103 -> 114[label="",style="solid", color="black", weight=3];
104[label="primIntToChar (primMinusInt (Pos vuy30) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];104 -> 115[label="",style="solid", color="black", weight=3];
105[label="primMinusInt (truncate vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];105 -> 116[label="",style="solid", color="black", weight=3];
106[label="toEnum10 (primEqInt (primMinusInt (fromEnum LT) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum LT) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];106 -> 117[label="",style="solid", color="black", weight=3];
107[label="toEnum10 (primEqInt (primMinusInt (fromEnum EQ) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum EQ) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];107 -> 118[label="",style="solid", color="black", weight=3];
108[label="toEnum10 (primEqInt (primMinusInt (fromEnum GT) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum GT) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];108 -> 119[label="",style="solid", color="black", weight=3];
109[label="(-) fromEnum vuy3 Pos (Succ Zero)",fontsize=16,color="black",shape="box"];109 -> 120[label="",style="solid", color="black", weight=3];
110[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];110 -> 121[label="",style="solid", color="black", weight=3];
111[label="primMinusInt (truncateM vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];111 -> 122[label="",style="solid", color="black", weight=3];
112[label="toEnum4 (primEqInt (primMinusInt (Pos Zero) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos Zero) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];112 -> 123[label="",style="solid", color="black", weight=3];
113[label="toEnum2 (primEqInt (primMinusInt (Pos Zero) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos Zero) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];113 -> 124[label="",style="solid", color="black", weight=3];
114[label="toEnum2 (primEqInt (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];114 -> 125[label="",style="solid", color="black", weight=3];
115[label="primIntToChar (primMinusNat vuy30 (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2569[label="vuy30/Succ vuy300",fontsize=10,color="white",style="solid",shape="box"];115 -> 2569[label="",style="solid", color="burlywood", weight=9];
2569 -> 126[label="",style="solid", color="burlywood", weight=3];
2570[label="vuy30/Zero",fontsize=10,color="white",style="solid",shape="box"];115 -> 2570[label="",style="solid", color="burlywood", weight=9];
2570 -> 127[label="",style="solid", color="burlywood", weight=3];
116[label="primMinusInt (truncateM vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];116 -> 128[label="",style="solid", color="black", weight=3];
117[label="toEnum10 (primEqInt (primMinusInt (Pos Zero) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos Zero) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];117 -> 129[label="",style="solid", color="black", weight=3];
118[label="toEnum10 (primEqInt (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];118 -> 130[label="",style="solid", color="black", weight=3];
119[label="toEnum10 (primEqInt (primMinusInt (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos (Succ (Succ Zero))) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];119 -> 131[label="",style="solid", color="black", weight=3];
120[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];120 -> 132[label="",style="solid", color="black", weight=3];
121[label="(-) fromEnum vuy3 Pos (Succ Zero)",fontsize=16,color="black",shape="box"];121 -> 133[label="",style="solid", color="black", weight=3];
122[label="primMinusInt (truncateM0 vuy3 (truncateVu6 vuy3)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];122 -> 134[label="",style="solid", color="black", weight=3];
123[label="toEnum4 (primEqInt (primMinusNat Zero (Succ Zero)) (Pos Zero)) (primMinusNat Zero (Succ Zero))",fontsize=16,color="black",shape="box"];123 -> 135[label="",style="solid", color="black", weight=3];
124[label="toEnum2 (primEqInt (primMinusNat Zero (Succ Zero)) (Pos Zero)) (primMinusNat Zero (Succ Zero))",fontsize=16,color="black",shape="box"];124 -> 136[label="",style="solid", color="black", weight=3];
125[label="toEnum2 (primEqInt (primMinusNat (Succ Zero) (Succ Zero)) (Pos Zero)) (primMinusNat (Succ Zero) (Succ Zero))",fontsize=16,color="black",shape="box"];125 -> 137[label="",style="solid", color="black", weight=3];
126[label="primIntToChar (primMinusNat (Succ vuy300) (Succ Zero))",fontsize=16,color="black",shape="box"];126 -> 138[label="",style="solid", color="black", weight=3];
127[label="primIntToChar (primMinusNat Zero (Succ Zero))",fontsize=16,color="black",shape="box"];127 -> 139[label="",style="solid", color="black", weight=3];
128[label="primMinusInt (truncateM0 vuy3 (truncateVu6 vuy3)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];128 -> 140[label="",style="solid", color="black", weight=3];
129[label="toEnum10 (primEqInt (primMinusNat Zero (Succ Zero)) (Pos Zero)) (primMinusNat Zero (Succ Zero))",fontsize=16,color="black",shape="box"];129 -> 141[label="",style="solid", color="black", weight=3];
130[label="toEnum10 (primEqInt (primMinusNat (Succ Zero) (Succ Zero)) (Pos Zero)) (primMinusNat (Succ Zero) (Succ Zero))",fontsize=16,color="black",shape="box"];130 -> 142[label="",style="solid", color="black", weight=3];
131[label="toEnum10 (primEqInt (primMinusNat (Succ (Succ Zero)) (Succ Zero)) (Pos Zero)) (primMinusNat (Succ (Succ Zero)) (Succ Zero))",fontsize=16,color="black",shape="box"];131 -> 143[label="",style="solid", color="black", weight=3];
132[label="primMinusInt (truncate vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];132 -> 144[label="",style="solid", color="black", weight=3];
133[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];133 -> 145[label="",style="solid", color="black", weight=3];
134[label="primMinusInt (truncateM0 vuy3 (properFraction vuy3)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];134 -> 146[label="",style="solid", color="black", weight=3];
135[label="toEnum4 (primEqInt (Neg (Succ Zero)) (Pos Zero)) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];135 -> 147[label="",style="solid", color="black", weight=3];
136[label="toEnum2 (primEqInt (Neg (Succ Zero)) (Pos Zero)) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];136 -> 148[label="",style="solid", color="black", weight=3];
137[label="toEnum2 (primEqInt (primMinusNat Zero Zero) (Pos Zero)) (primMinusNat Zero Zero)",fontsize=16,color="black",shape="box"];137 -> 149[label="",style="solid", color="black", weight=3];
138[label="primIntToChar (primMinusNat vuy300 Zero)",fontsize=16,color="burlywood",shape="box"];2571[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];138 -> 2571[label="",style="solid", color="burlywood", weight=9];
2571 -> 150[label="",style="solid", color="burlywood", weight=3];
2572[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];138 -> 2572[label="",style="solid", color="burlywood", weight=9];
2572 -> 151[label="",style="solid", color="burlywood", weight=3];
139[label="primIntToChar (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];139 -> 152[label="",style="solid", color="black", weight=3];
140[label="primMinusInt (truncateM0 vuy3 (properFraction vuy3)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];140 -> 153[label="",style="solid", color="black", weight=3];
141[label="toEnum10 (primEqInt (Neg (Succ Zero)) (Pos Zero)) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];141 -> 154[label="",style="solid", color="black", weight=3];
142[label="toEnum10 (primEqInt (primMinusNat Zero Zero) (Pos Zero)) (primMinusNat Zero Zero)",fontsize=16,color="black",shape="box"];142 -> 155[label="",style="solid", color="black", weight=3];
143[label="toEnum10 (primEqInt (primMinusNat (Succ Zero) Zero) (Pos Zero)) (primMinusNat (Succ Zero) Zero)",fontsize=16,color="black",shape="box"];143 -> 156[label="",style="solid", color="black", weight=3];
144[label="primMinusInt (truncateM vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];144 -> 157[label="",style="solid", color="black", weight=3];
145[label="primMinusInt (truncate vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];145 -> 158[label="",style="solid", color="black", weight=3];
146[label="primMinusInt (truncateM0 vuy3 (floatProperFractionDouble vuy3)) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2573[label="vuy3/Double vuy30 vuy31",fontsize=10,color="white",style="solid",shape="box"];146 -> 2573[label="",style="solid", color="burlywood", weight=9];
2573 -> 159[label="",style="solid", color="burlywood", weight=3];
147[label="toEnum4 False (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];147 -> 160[label="",style="solid", color="black", weight=3];
148[label="toEnum2 False (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];148 -> 161[label="",style="solid", color="black", weight=3];
149[label="toEnum2 (primEqInt (Pos Zero) (Pos Zero)) (Pos Zero)",fontsize=16,color="black",shape="box"];149 -> 162[label="",style="solid", color="black", weight=3];
150[label="primIntToChar (primMinusNat (Succ vuy3000) Zero)",fontsize=16,color="black",shape="box"];150 -> 163[label="",style="solid", color="black", weight=3];
151[label="primIntToChar (primMinusNat Zero Zero)",fontsize=16,color="black",shape="box"];151 -> 164[label="",style="solid", color="black", weight=3];
152[label="error []",fontsize=16,color="red",shape="box"];153[label="primMinusInt (truncateM0 vuy3 (floatProperFractionFloat vuy3)) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2574[label="vuy3/Float vuy30 vuy31",fontsize=10,color="white",style="solid",shape="box"];153 -> 2574[label="",style="solid", color="burlywood", weight=9];
2574 -> 165[label="",style="solid", color="burlywood", weight=3];
154[label="toEnum10 False (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];154 -> 166[label="",style="solid", color="black", weight=3];
155[label="toEnum10 (primEqInt (Pos Zero) (Pos Zero)) (Pos Zero)",fontsize=16,color="black",shape="box"];155 -> 167[label="",style="solid", color="black", weight=3];
156[label="toEnum10 (primEqInt (Pos (Succ Zero)) (Pos Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];156 -> 168[label="",style="solid", color="black", weight=3];
157[label="primMinusInt (truncateM0 vuy3 (truncateVu6 vuy3)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];157 -> 169[label="",style="solid", color="black", weight=3];
158[label="primMinusInt (truncateM vuy3) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];158 -> 170[label="",style="solid", color="black", weight=3];
159[label="primMinusInt (truncateM0 (Double vuy30 vuy31) (floatProperFractionDouble (Double vuy30 vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];159 -> 171[label="",style="solid", color="black", weight=3];
160[label="error []",fontsize=16,color="red",shape="box"];161[label="toEnum1 (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];161 -> 172[label="",style="solid", color="black", weight=3];
162[label="toEnum2 True (Pos Zero)",fontsize=16,color="black",shape="box"];162 -> 173[label="",style="solid", color="black", weight=3];
163[label="primIntToChar (Pos (Succ vuy3000))",fontsize=16,color="black",shape="box"];163 -> 174[label="",style="solid", color="black", weight=3];
164[label="primIntToChar (Pos Zero)",fontsize=16,color="black",shape="box"];164 -> 175[label="",style="solid", color="black", weight=3];
165[label="primMinusInt (truncateM0 (Float vuy30 vuy31) (floatProperFractionFloat (Float vuy30 vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];165 -> 176[label="",style="solid", color="black", weight=3];
166[label="toEnum9 (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];166 -> 177[label="",style="solid", color="black", weight=3];
167[label="toEnum10 True (Pos Zero)",fontsize=16,color="black",shape="box"];167 -> 178[label="",style="solid", color="black", weight=3];
168[label="toEnum10 False (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];168 -> 179[label="",style="solid", color="black", weight=3];
169[label="primMinusInt (truncateM0 vuy3 (properFraction vuy3)) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2575[label="vuy3/vuy30 :% vuy31",fontsize=10,color="white",style="solid",shape="box"];169 -> 2575[label="",style="solid", color="burlywood", weight=9];
2575 -> 180[label="",style="solid", color="burlywood", weight=3];
170[label="primMinusInt (truncateM0 vuy3 (truncateVu6 vuy3)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];170 -> 181[label="",style="solid", color="black", weight=3];
171[label="primMinusInt (truncateM0 (Double vuy30 vuy31) (fromInt (vuy30 `quot` vuy31),Double vuy30 vuy31 - fromInt (vuy30 `quot` vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];171 -> 182[label="",style="solid", color="black", weight=3];
172[label="toEnum0 (Neg (Succ Zero) == Pos (Succ Zero)) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];172 -> 183[label="",style="solid", color="black", weight=3];
173[label="False",fontsize=16,color="green",shape="box"];174[label="Char (Succ vuy3000)",fontsize=16,color="green",shape="box"];175[label="Char Zero",fontsize=16,color="green",shape="box"];176[label="primMinusInt (truncateM0 (Float vuy30 vuy31) (fromInt (vuy30 `quot` vuy31),Float vuy30 vuy31 - fromInt (vuy30 `quot` vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];176 -> 184[label="",style="solid", color="black", weight=3];
177[label="toEnum8 (Neg (Succ Zero) == Pos (Succ Zero)) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];177 -> 185[label="",style="solid", color="black", weight=3];
178[label="LT",fontsize=16,color="green",shape="box"];179[label="toEnum9 (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];179 -> 186[label="",style="solid", color="black", weight=3];
180[label="primMinusInt (truncateM0 (vuy30 :% vuy31) (properFraction (vuy30 :% vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];180 -> 187[label="",style="solid", color="black", weight=3];
181[label="primMinusInt (truncateM0 vuy3 (properFraction vuy3)) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2576[label="vuy3/vuy30 :% vuy31",fontsize=10,color="white",style="solid",shape="box"];181 -> 2576[label="",style="solid", color="burlywood", weight=9];
2576 -> 188[label="",style="solid", color="burlywood", weight=3];
182[label="primMinusInt (fromInt (vuy30 `quot` vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];182 -> 189[label="",style="solid", color="black", weight=3];
183[label="toEnum0 (primEqInt (Neg (Succ Zero)) (Pos (Succ Zero))) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];183 -> 190[label="",style="solid", color="black", weight=3];
184 -> 182[label="",style="dashed", color="red", weight=0];
184[label="primMinusInt (fromInt (vuy30 `quot` vuy31)) (Pos (Succ Zero))",fontsize=16,color="magenta"];184 -> 191[label="",style="dashed", color="magenta", weight=3];
184 -> 192[label="",style="dashed", color="magenta", weight=3];
185[label="toEnum8 (primEqInt (Neg (Succ Zero)) (Pos (Succ Zero))) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];185 -> 193[label="",style="solid", color="black", weight=3];
186[label="toEnum8 (Pos (Succ Zero) == Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];186 -> 194[label="",style="solid", color="black", weight=3];
187[label="primMinusInt (truncateM0 (vuy30 :% vuy31) (fromIntegral (properFractionQ vuy30 vuy31),properFractionR vuy30 vuy31 :% vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];187 -> 195[label="",style="solid", color="black", weight=3];
188[label="primMinusInt (truncateM0 (vuy30 :% vuy31) (properFraction (vuy30 :% vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];188 -> 196[label="",style="solid", color="black", weight=3];
189[label="primMinusInt (vuy30 `quot` vuy31) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];189 -> 197[label="",style="solid", color="black", weight=3];
190[label="toEnum0 False (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];190 -> 198[label="",style="solid", color="black", weight=3];
191[label="vuy30",fontsize=16,color="green",shape="box"];192[label="vuy31",fontsize=16,color="green",shape="box"];193[label="toEnum8 False (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];193 -> 199[label="",style="solid", color="black", weight=3];
194[label="toEnum8 (primEqInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];194 -> 200[label="",style="solid", color="black", weight=3];
195[label="primMinusInt (fromIntegral (properFractionQ vuy30 vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];195 -> 201[label="",style="solid", color="black", weight=3];
196[label="primMinusInt (truncateM0 (vuy30 :% vuy31) (fromIntegral (properFractionQ vuy30 vuy31),properFractionR vuy30 vuy31 :% vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];196 -> 202[label="",style="solid", color="black", weight=3];
197[label="primMinusInt (primQuotInt vuy30 vuy31) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="triangle"];2578[label="vuy30/Pos vuy300",fontsize=10,color="white",style="solid",shape="box"];197 -> 2578[label="",style="solid", color="burlywood", weight=9];
2578 -> 203[label="",style="solid", color="burlywood", weight=3];
2579[label="vuy30/Neg vuy300",fontsize=10,color="white",style="solid",shape="box"];197 -> 2579[label="",style="solid", color="burlywood", weight=9];
2579 -> 204[label="",style="solid", color="burlywood", weight=3];
198[label="error []",fontsize=16,color="red",shape="box"];199[label="toEnum7 (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];199 -> 205[label="",style="solid", color="black", weight=3];
200[label="toEnum8 (primEqNat Zero Zero) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];200 -> 206[label="",style="solid", color="black", weight=3];
201[label="primMinusInt (fromInteger . toInteger) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];201 -> 207[label="",style="solid", color="black", weight=3];
202[label="primMinusInt (fromIntegral (properFractionQ vuy30 vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];202 -> 208[label="",style="solid", color="black", weight=3];
203[label="primMinusInt (primQuotInt (Pos vuy300) vuy31) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2580[label="vuy31/Pos vuy310",fontsize=10,color="white",style="solid",shape="box"];203 -> 2580[label="",style="solid", color="burlywood", weight=9];
2580 -> 209[label="",style="solid", color="burlywood", weight=3];
2581[label="vuy31/Neg vuy310",fontsize=10,color="white",style="solid",shape="box"];203 -> 2581[label="",style="solid", color="burlywood", weight=9];
2581 -> 210[label="",style="solid", color="burlywood", weight=3];
204[label="primMinusInt (primQuotInt (Neg vuy300) vuy31) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2582[label="vuy31/Pos vuy310",fontsize=10,color="white",style="solid",shape="box"];204 -> 2582[label="",style="solid", color="burlywood", weight=9];
2582 -> 211[label="",style="solid", color="burlywood", weight=3];
2583[label="vuy31/Neg vuy310",fontsize=10,color="white",style="solid",shape="box"];204 -> 2583[label="",style="solid", color="burlywood", weight=9];
2583 -> 212[label="",style="solid", color="burlywood", weight=3];
205[label="toEnum6 (Neg (Succ Zero) == Pos (Succ (Succ Zero))) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];205 -> 213[label="",style="solid", color="black", weight=3];
206[label="toEnum8 True (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];206 -> 214[label="",style="solid", color="black", weight=3];
207[label="primMinusInt (fromInteger (toInteger (properFractionQ vuy30 vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];207 -> 215[label="",style="solid", color="black", weight=3];
208[label="primMinusInt (fromInteger . toInteger) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];208 -> 216[label="",style="solid", color="black", weight=3];
209[label="primMinusInt (primQuotInt (Pos vuy300) (Pos vuy310)) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2584[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];209 -> 2584[label="",style="solid", color="burlywood", weight=9];
2584 -> 217[label="",style="solid", color="burlywood", weight=3];
2585[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];209 -> 2585[label="",style="solid", color="burlywood", weight=9];
2585 -> 218[label="",style="solid", color="burlywood", weight=3];
210[label="primMinusInt (primQuotInt (Pos vuy300) (Neg vuy310)) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2586[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];210 -> 2586[label="",style="solid", color="burlywood", weight=9];
2586 -> 219[label="",style="solid", color="burlywood", weight=3];
2587[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];210 -> 2587[label="",style="solid", color="burlywood", weight=9];
2587 -> 220[label="",style="solid", color="burlywood", weight=3];
211[label="primMinusInt (primQuotInt (Neg vuy300) (Pos vuy310)) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2588[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];211 -> 2588[label="",style="solid", color="burlywood", weight=9];
2588 -> 221[label="",style="solid", color="burlywood", weight=3];
2589[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];211 -> 2589[label="",style="solid", color="burlywood", weight=9];
2589 -> 222[label="",style="solid", color="burlywood", weight=3];
212[label="primMinusInt (primQuotInt (Neg vuy300) (Neg vuy310)) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2590[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];212 -> 2590[label="",style="solid", color="burlywood", weight=9];
2590 -> 223[label="",style="solid", color="burlywood", weight=3];
2591[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];212 -> 2591[label="",style="solid", color="burlywood", weight=9];
2591 -> 224[label="",style="solid", color="burlywood", weight=3];
213[label="toEnum6 (primEqInt (Neg (Succ Zero)) (Pos (Succ (Succ Zero)))) (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];213 -> 225[label="",style="solid", color="black", weight=3];
214[label="EQ",fontsize=16,color="green",shape="box"];215[label="primMinusInt (fromInteger (Integer (properFractionQ vuy30 vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];215 -> 226[label="",style="solid", color="black", weight=3];
216[label="primMinusInt (fromInteger (toInteger (properFractionQ vuy30 vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];216 -> 227[label="",style="solid", color="black", weight=3];
217[label="primMinusInt (primQuotInt (Pos vuy300) (Pos (Succ vuy3100))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];217 -> 228[label="",style="solid", color="black", weight=3];
218[label="primMinusInt (primQuotInt (Pos vuy300) (Pos Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];218 -> 229[label="",style="solid", color="black", weight=3];
219[label="primMinusInt (primQuotInt (Pos vuy300) (Neg (Succ vuy3100))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];219 -> 230[label="",style="solid", color="black", weight=3];
220[label="primMinusInt (primQuotInt (Pos vuy300) (Neg Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];220 -> 231[label="",style="solid", color="black", weight=3];
221[label="primMinusInt (primQuotInt (Neg vuy300) (Pos (Succ vuy3100))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];221 -> 232[label="",style="solid", color="black", weight=3];
222[label="primMinusInt (primQuotInt (Neg vuy300) (Pos Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];222 -> 233[label="",style="solid", color="black", weight=3];
223[label="primMinusInt (primQuotInt (Neg vuy300) (Neg (Succ vuy3100))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];223 -> 234[label="",style="solid", color="black", weight=3];
224[label="primMinusInt (primQuotInt (Neg vuy300) (Neg Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];224 -> 235[label="",style="solid", color="black", weight=3];
225[label="toEnum6 False (Neg (Succ Zero))",fontsize=16,color="black",shape="box"];225 -> 236[label="",style="solid", color="black", weight=3];
226[label="primMinusInt (properFractionQ vuy30 vuy31) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];226 -> 237[label="",style="solid", color="black", weight=3];
227[label="primMinusInt (fromInteger (properFractionQ vuy30 vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];227 -> 238[label="",style="solid", color="black", weight=3];
228[label="primMinusInt (Pos (primDivNatS vuy300 (Succ vuy3100))) (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];228 -> 239[label="",style="solid", color="black", weight=3];
229[label="primMinusInt (error []) (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];229 -> 240[label="",style="solid", color="black", weight=3];
230[label="primMinusInt (Neg (primDivNatS vuy300 (Succ vuy3100))) (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];230 -> 241[label="",style="solid", color="black", weight=3];
231 -> 229[label="",style="dashed", color="red", weight=0];
231[label="primMinusInt (error []) (Pos (Succ Zero))",fontsize=16,color="magenta"];232 -> 230[label="",style="dashed", color="red", weight=0];
232[label="primMinusInt (Neg (primDivNatS vuy300 (Succ vuy3100))) (Pos (Succ Zero))",fontsize=16,color="magenta"];232 -> 242[label="",style="dashed", color="magenta", weight=3];
232 -> 243[label="",style="dashed", color="magenta", weight=3];
233 -> 229[label="",style="dashed", color="red", weight=0];
233[label="primMinusInt (error []) (Pos (Succ Zero))",fontsize=16,color="magenta"];234 -> 228[label="",style="dashed", color="red", weight=0];
234[label="primMinusInt (Pos (primDivNatS vuy300 (Succ vuy3100))) (Pos (Succ Zero))",fontsize=16,color="magenta"];234 -> 244[label="",style="dashed", color="magenta", weight=3];
234 -> 245[label="",style="dashed", color="magenta", weight=3];
235 -> 229[label="",style="dashed", color="red", weight=0];
235[label="primMinusInt (error []) (Pos (Succ Zero))",fontsize=16,color="magenta"];236[label="error []",fontsize=16,color="red",shape="box"];237[label="primMinusInt (properFractionQ1 vuy30 vuy31 (properFractionVu30 vuy30 vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];237 -> 246[label="",style="solid", color="black", weight=3];
238[label="primMinusInt (fromInteger (properFractionQ1 vuy30 vuy31 (properFractionVu30 vuy30 vuy31))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];238 -> 247[label="",style="solid", color="black", weight=3];
239[label="primMinusNat (primDivNatS vuy300 (Succ vuy3100)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2597[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];239 -> 2597[label="",style="solid", color="burlywood", weight=9];
2597 -> 248[label="",style="solid", color="burlywood", weight=3];
2598[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];239 -> 2598[label="",style="solid", color="burlywood", weight=9];
2598 -> 249[label="",style="solid", color="burlywood", weight=3];
240[label="error []",fontsize=16,color="red",shape="box"];241[label="Neg (primPlusNat (primDivNatS vuy300 (Succ vuy3100)) (Succ Zero))",fontsize=16,color="green",shape="box"];241 -> 250[label="",style="dashed", color="green", weight=3];
242[label="vuy300",fontsize=16,color="green",shape="box"];243[label="vuy3100",fontsize=16,color="green",shape="box"];244[label="vuy300",fontsize=16,color="green",shape="box"];245[label="vuy3100",fontsize=16,color="green",shape="box"];246[label="primMinusInt (properFractionQ1 vuy30 vuy31 (quotRem vuy30 vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];246 -> 251[label="",style="solid", color="black", weight=3];
247[label="primMinusInt (fromInteger (properFractionQ1 vuy30 vuy31 (quotRem vuy30 vuy31))) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2599[label="vuy30/Integer vuy300",fontsize=10,color="white",style="solid",shape="box"];247 -> 2599[label="",style="solid", color="burlywood", weight=9];
2599 -> 252[label="",style="solid", color="burlywood", weight=3];
248[label="primMinusNat (primDivNatS (Succ vuy3000) (Succ vuy3100)) (Succ Zero)",fontsize=16,color="black",shape="box"];248 -> 253[label="",style="solid", color="black", weight=3];
249[label="primMinusNat (primDivNatS Zero (Succ vuy3100)) (Succ Zero)",fontsize=16,color="black",shape="box"];249 -> 254[label="",style="solid", color="black", weight=3];
250[label="primPlusNat (primDivNatS vuy300 (Succ vuy3100)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2600[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];250 -> 2600[label="",style="solid", color="burlywood", weight=9];
2600 -> 255[label="",style="solid", color="burlywood", weight=3];
2601[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];250 -> 2601[label="",style="solid", color="burlywood", weight=9];
2601 -> 256[label="",style="solid", color="burlywood", weight=3];
251[label="primMinusInt (properFractionQ1 vuy30 vuy31 (primQrmInt vuy30 vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];251 -> 257[label="",style="solid", color="black", weight=3];
252[label="primMinusInt (fromInteger (properFractionQ1 (Integer vuy300) vuy31 (quotRem (Integer vuy300) vuy31))) (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2602[label="vuy31/Integer vuy310",fontsize=10,color="white",style="solid",shape="box"];252 -> 2602[label="",style="solid", color="burlywood", weight=9];
2602 -> 258[label="",style="solid", color="burlywood", weight=3];
253[label="primMinusNat (primDivNatS0 vuy3000 vuy3100 (primGEqNatS vuy3000 vuy3100)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2603[label="vuy3000/Succ vuy30000",fontsize=10,color="white",style="solid",shape="box"];253 -> 2603[label="",style="solid", color="burlywood", weight=9];
2603 -> 259[label="",style="solid", color="burlywood", weight=3];
2604[label="vuy3000/Zero",fontsize=10,color="white",style="solid",shape="box"];253 -> 2604[label="",style="solid", color="burlywood", weight=9];
2604 -> 260[label="",style="solid", color="burlywood", weight=3];
254[label="primMinusNat Zero (Succ Zero)",fontsize=16,color="black",shape="triangle"];254 -> 261[label="",style="solid", color="black", weight=3];
255[label="primPlusNat (primDivNatS (Succ vuy3000) (Succ vuy3100)) (Succ Zero)",fontsize=16,color="black",shape="box"];255 -> 262[label="",style="solid", color="black", weight=3];
256[label="primPlusNat (primDivNatS Zero (Succ vuy3100)) (Succ Zero)",fontsize=16,color="black",shape="box"];256 -> 263[label="",style="solid", color="black", weight=3];
257[label="primMinusInt (properFractionQ1 vuy30 vuy31 (primQuotInt vuy30 vuy31,primRemInt vuy30 vuy31)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];257 -> 264[label="",style="solid", color="black", weight=3];
258[label="primMinusInt (fromInteger (properFractionQ1 (Integer vuy300) (Integer vuy310) (quotRem (Integer vuy300) (Integer vuy310)))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];258 -> 265[label="",style="solid", color="black", weight=3];
259[label="primMinusNat (primDivNatS0 (Succ vuy30000) vuy3100 (primGEqNatS (Succ vuy30000) vuy3100)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2605[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];259 -> 2605[label="",style="solid", color="burlywood", weight=9];
2605 -> 266[label="",style="solid", color="burlywood", weight=3];
2606[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];259 -> 2606[label="",style="solid", color="burlywood", weight=9];
2606 -> 267[label="",style="solid", color="burlywood", weight=3];
260[label="primMinusNat (primDivNatS0 Zero vuy3100 (primGEqNatS Zero vuy3100)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2607[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];260 -> 2607[label="",style="solid", color="burlywood", weight=9];
2607 -> 268[label="",style="solid", color="burlywood", weight=3];
2608[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];260 -> 2608[label="",style="solid", color="burlywood", weight=9];
2608 -> 269[label="",style="solid", color="burlywood", weight=3];
261[label="Neg (Succ Zero)",fontsize=16,color="green",shape="box"];262[label="primPlusNat (primDivNatS0 vuy3000 vuy3100 (primGEqNatS vuy3000 vuy3100)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2609[label="vuy3000/Succ vuy30000",fontsize=10,color="white",style="solid",shape="box"];262 -> 2609[label="",style="solid", color="burlywood", weight=9];
2609 -> 270[label="",style="solid", color="burlywood", weight=3];
2610[label="vuy3000/Zero",fontsize=10,color="white",style="solid",shape="box"];262 -> 2610[label="",style="solid", color="burlywood", weight=9];
2610 -> 271[label="",style="solid", color="burlywood", weight=3];
263[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="black",shape="triangle"];263 -> 272[label="",style="solid", color="black", weight=3];
264 -> 197[label="",style="dashed", color="red", weight=0];
264[label="primMinusInt (primQuotInt vuy30 vuy31) (Pos (Succ Zero))",fontsize=16,color="magenta"];264 -> 273[label="",style="dashed", color="magenta", weight=3];
264 -> 274[label="",style="dashed", color="magenta", weight=3];
265[label="primMinusInt (fromInteger (properFractionQ1 (Integer vuy300) (Integer vuy310) (Integer (primQuotInt vuy300 vuy310),Integer (primRemInt vuy300 vuy310)))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];265 -> 275[label="",style="solid", color="black", weight=3];
266[label="primMinusNat (primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS (Succ vuy30000) (Succ vuy31000))) (Succ Zero)",fontsize=16,color="black",shape="box"];266 -> 276[label="",style="solid", color="black", weight=3];
267[label="primMinusNat (primDivNatS0 (Succ vuy30000) Zero (primGEqNatS (Succ vuy30000) Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];267 -> 277[label="",style="solid", color="black", weight=3];
268[label="primMinusNat (primDivNatS0 Zero (Succ vuy31000) (primGEqNatS Zero (Succ vuy31000))) (Succ Zero)",fontsize=16,color="black",shape="box"];268 -> 278[label="",style="solid", color="black", weight=3];
269[label="primMinusNat (primDivNatS0 Zero Zero (primGEqNatS Zero Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];269 -> 279[label="",style="solid", color="black", weight=3];
270[label="primPlusNat (primDivNatS0 (Succ vuy30000) vuy3100 (primGEqNatS (Succ vuy30000) vuy3100)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2612[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];270 -> 2612[label="",style="solid", color="burlywood", weight=9];
2612 -> 280[label="",style="solid", color="burlywood", weight=3];
2613[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];270 -> 2613[label="",style="solid", color="burlywood", weight=9];
2613 -> 281[label="",style="solid", color="burlywood", weight=3];
271[label="primPlusNat (primDivNatS0 Zero vuy3100 (primGEqNatS Zero vuy3100)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2614[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];271 -> 2614[label="",style="solid", color="burlywood", weight=9];
2614 -> 282[label="",style="solid", color="burlywood", weight=3];
2615[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];271 -> 2615[label="",style="solid", color="burlywood", weight=9];
2615 -> 283[label="",style="solid", color="burlywood", weight=3];
272[label="Succ Zero",fontsize=16,color="green",shape="box"];273[label="vuy30",fontsize=16,color="green",shape="box"];274[label="vuy31",fontsize=16,color="green",shape="box"];275[label="primMinusInt (fromInteger (Integer (primQuotInt vuy300 vuy310))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];275 -> 284[label="",style="solid", color="black", weight=3];
276 -> 872[label="",style="dashed", color="red", weight=0];
276[label="primMinusNat (primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS vuy30000 vuy31000)) (Succ Zero)",fontsize=16,color="magenta"];276 -> 873[label="",style="dashed", color="magenta", weight=3];
276 -> 874[label="",style="dashed", color="magenta", weight=3];
276 -> 875[label="",style="dashed", color="magenta", weight=3];
276 -> 876[label="",style="dashed", color="magenta", weight=3];
277[label="primMinusNat (primDivNatS0 (Succ vuy30000) Zero True) (Succ Zero)",fontsize=16,color="black",shape="box"];277 -> 287[label="",style="solid", color="black", weight=3];
278[label="primMinusNat (primDivNatS0 Zero (Succ vuy31000) False) (Succ Zero)",fontsize=16,color="black",shape="box"];278 -> 288[label="",style="solid", color="black", weight=3];
279[label="primMinusNat (primDivNatS0 Zero Zero True) (Succ Zero)",fontsize=16,color="black",shape="box"];279 -> 289[label="",style="solid", color="black", weight=3];
280[label="primPlusNat (primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS (Succ vuy30000) (Succ vuy31000))) (Succ Zero)",fontsize=16,color="black",shape="box"];280 -> 290[label="",style="solid", color="black", weight=3];
281[label="primPlusNat (primDivNatS0 (Succ vuy30000) Zero (primGEqNatS (Succ vuy30000) Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];281 -> 291[label="",style="solid", color="black", weight=3];
282[label="primPlusNat (primDivNatS0 Zero (Succ vuy31000) (primGEqNatS Zero (Succ vuy31000))) (Succ Zero)",fontsize=16,color="black",shape="box"];282 -> 292[label="",style="solid", color="black", weight=3];
283[label="primPlusNat (primDivNatS0 Zero Zero (primGEqNatS Zero Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];283 -> 293[label="",style="solid", color="black", weight=3];
284 -> 197[label="",style="dashed", color="red", weight=0];
284[label="primMinusInt (primQuotInt vuy300 vuy310) (Pos (Succ Zero))",fontsize=16,color="magenta"];284 -> 294[label="",style="dashed", color="magenta", weight=3];
284 -> 295[label="",style="dashed", color="magenta", weight=3];
873[label="vuy31000",fontsize=16,color="green",shape="box"];874[label="vuy31000",fontsize=16,color="green",shape="box"];875[label="vuy30000",fontsize=16,color="green",shape="box"];876[label="vuy30000",fontsize=16,color="green",shape="box"];872[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) (primGEqNatS vuy40 vuy41)) (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];2618[label="vuy40/Succ vuy400",fontsize=10,color="white",style="solid",shape="box"];872 -> 2618[label="",style="solid", color="burlywood", weight=9];
2618 -> 913[label="",style="solid", color="burlywood", weight=3];
2619[label="vuy40/Zero",fontsize=10,color="white",style="solid",shape="box"];872 -> 2619[label="",style="solid", color="burlywood", weight=9];
2619 -> 914[label="",style="solid", color="burlywood", weight=3];
287[label="primMinusNat (Succ (primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero))) (Succ Zero)",fontsize=16,color="black",shape="box"];287 -> 300[label="",style="solid", color="black", weight=3];
288 -> 254[label="",style="dashed", color="red", weight=0];
288[label="primMinusNat Zero (Succ Zero)",fontsize=16,color="magenta"];289[label="primMinusNat (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))) (Succ Zero)",fontsize=16,color="black",shape="box"];289 -> 301[label="",style="solid", color="black", weight=3];
290 -> 945[label="",style="dashed", color="red", weight=0];
290[label="primPlusNat (primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS vuy30000 vuy31000)) (Succ Zero)",fontsize=16,color="magenta"];290 -> 946[label="",style="dashed", color="magenta", weight=3];
290 -> 947[label="",style="dashed", color="magenta", weight=3];
290 -> 948[label="",style="dashed", color="magenta", weight=3];
290 -> 949[label="",style="dashed", color="magenta", weight=3];
291[label="primPlusNat (primDivNatS0 (Succ vuy30000) Zero True) (Succ Zero)",fontsize=16,color="black",shape="box"];291 -> 304[label="",style="solid", color="black", weight=3];
292[label="primPlusNat (primDivNatS0 Zero (Succ vuy31000) False) (Succ Zero)",fontsize=16,color="black",shape="box"];292 -> 305[label="",style="solid", color="black", weight=3];
293[label="primPlusNat (primDivNatS0 Zero Zero True) (Succ Zero)",fontsize=16,color="black",shape="box"];293 -> 306[label="",style="solid", color="black", weight=3];
294[label="vuy300",fontsize=16,color="green",shape="box"];295[label="vuy310",fontsize=16,color="green",shape="box"];913[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) (primGEqNatS (Succ vuy400) vuy41)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2622[label="vuy41/Succ vuy410",fontsize=10,color="white",style="solid",shape="box"];913 -> 2622[label="",style="solid", color="burlywood", weight=9];
2622 -> 919[label="",style="solid", color="burlywood", weight=3];
2623[label="vuy41/Zero",fontsize=10,color="white",style="solid",shape="box"];913 -> 2623[label="",style="solid", color="burlywood", weight=9];
2623 -> 920[label="",style="solid", color="burlywood", weight=3];
914[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) (primGEqNatS Zero vuy41)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2624[label="vuy41/Succ vuy410",fontsize=10,color="white",style="solid",shape="box"];914 -> 2624[label="",style="solid", color="burlywood", weight=9];
2624 -> 921[label="",style="solid", color="burlywood", weight=3];
2625[label="vuy41/Zero",fontsize=10,color="white",style="solid",shape="box"];914 -> 2625[label="",style="solid", color="burlywood", weight=9];
2625 -> 922[label="",style="solid", color="burlywood", weight=3];
300 -> 1353[label="",style="dashed", color="red", weight=0];
300[label="primMinusNat (primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero)) Zero",fontsize=16,color="magenta"];300 -> 1354[label="",style="dashed", color="magenta", weight=3];
300 -> 1355[label="",style="dashed", color="magenta", weight=3];
300 -> 1356[label="",style="dashed", color="magenta", weight=3];
301 -> 1353[label="",style="dashed", color="red", weight=0];
301[label="primMinusNat (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)) Zero",fontsize=16,color="magenta"];301 -> 1357[label="",style="dashed", color="magenta", weight=3];
301 -> 1358[label="",style="dashed", color="magenta", weight=3];
301 -> 1359[label="",style="dashed", color="magenta", weight=3];
946[label="vuy31000",fontsize=16,color="green",shape="box"];947[label="vuy30000",fontsize=16,color="green",shape="box"];948[label="vuy30000",fontsize=16,color="green",shape="box"];949[label="vuy31000",fontsize=16,color="green",shape="box"];945[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) (primGEqNatS vuy53 vuy54)) (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];2628[label="vuy53/Succ vuy530",fontsize=10,color="white",style="solid",shape="box"];945 -> 2628[label="",style="solid", color="burlywood", weight=9];
2628 -> 986[label="",style="solid", color="burlywood", weight=3];
2629[label="vuy53/Zero",fontsize=10,color="white",style="solid",shape="box"];945 -> 2629[label="",style="solid", color="burlywood", weight=9];
2629 -> 987[label="",style="solid", color="burlywood", weight=3];
304[label="primPlusNat (Succ (primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero))) (Succ Zero)",fontsize=16,color="black",shape="box"];304 -> 317[label="",style="solid", color="black", weight=3];
305 -> 263[label="",style="dashed", color="red", weight=0];
305[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="magenta"];306[label="primPlusNat (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))) (Succ Zero)",fontsize=16,color="black",shape="box"];306 -> 318[label="",style="solid", color="black", weight=3];
919[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) (primGEqNatS (Succ vuy400) (Succ vuy410))) (Succ Zero)",fontsize=16,color="black",shape="box"];919 -> 926[label="",style="solid", color="black", weight=3];
920[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) (primGEqNatS (Succ vuy400) Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];920 -> 927[label="",style="solid", color="black", weight=3];
921[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) (primGEqNatS Zero (Succ vuy410))) (Succ Zero)",fontsize=16,color="black",shape="box"];921 -> 928[label="",style="solid", color="black", weight=3];
922[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) (primGEqNatS Zero Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];922 -> 929[label="",style="solid", color="black", weight=3];
1354[label="Succ vuy30000",fontsize=16,color="green",shape="box"];1355[label="Zero",fontsize=16,color="green",shape="box"];1356[label="Zero",fontsize=16,color="green",shape="box"];1353[label="primMinusNat (primDivNatS (primMinusNatS vuy58 vuy59) (Succ vuy60)) Zero",fontsize=16,color="burlywood",shape="triangle"];2631[label="vuy58/Succ vuy580",fontsize=10,color="white",style="solid",shape="box"];1353 -> 2631[label="",style="solid", color="burlywood", weight=9];
2631 -> 1387[label="",style="solid", color="burlywood", weight=3];
2632[label="vuy58/Zero",fontsize=10,color="white",style="solid",shape="box"];1353 -> 2632[label="",style="solid", color="burlywood", weight=9];
2632 -> 1388[label="",style="solid", color="burlywood", weight=3];
1357[label="Zero",fontsize=16,color="green",shape="box"];1358[label="Zero",fontsize=16,color="green",shape="box"];1359[label="Zero",fontsize=16,color="green",shape="box"];986[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) (primGEqNatS (Succ vuy530) vuy54)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2633[label="vuy54/Succ vuy540",fontsize=10,color="white",style="solid",shape="box"];986 -> 2633[label="",style="solid", color="burlywood", weight=9];
2633 -> 989[label="",style="solid", color="burlywood", weight=3];
2634[label="vuy54/Zero",fontsize=10,color="white",style="solid",shape="box"];986 -> 2634[label="",style="solid", color="burlywood", weight=9];
2634 -> 990[label="",style="solid", color="burlywood", weight=3];
987[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) (primGEqNatS Zero vuy54)) (Succ Zero)",fontsize=16,color="burlywood",shape="box"];2635[label="vuy54/Succ vuy540",fontsize=10,color="white",style="solid",shape="box"];987 -> 2635[label="",style="solid", color="burlywood", weight=9];
2635 -> 991[label="",style="solid", color="burlywood", weight=3];
2636[label="vuy54/Zero",fontsize=10,color="white",style="solid",shape="box"];987 -> 2636[label="",style="solid", color="burlywood", weight=9];
2636 -> 992[label="",style="solid", color="burlywood", weight=3];
317[label="Succ (Succ (primPlusNat (primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero)) Zero))",fontsize=16,color="green",shape="box"];317 -> 330[label="",style="dashed", color="green", weight=3];
318[label="Succ (Succ (primPlusNat (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)) Zero))",fontsize=16,color="green",shape="box"];318 -> 331[label="",style="dashed", color="green", weight=3];
926 -> 872[label="",style="dashed", color="red", weight=0];
926[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) (primGEqNatS vuy400 vuy410)) (Succ Zero)",fontsize=16,color="magenta"];926 -> 932[label="",style="dashed", color="magenta", weight=3];
926 -> 933[label="",style="dashed", color="magenta", weight=3];
927[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) True) (Succ Zero)",fontsize=16,color="black",shape="triangle"];927 -> 934[label="",style="solid", color="black", weight=3];
928[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) False) (Succ Zero)",fontsize=16,color="black",shape="box"];928 -> 935[label="",style="solid", color="black", weight=3];
929 -> 927[label="",style="dashed", color="red", weight=0];
929[label="primMinusNat (primDivNatS0 (Succ vuy38) (Succ vuy39) True) (Succ Zero)",fontsize=16,color="magenta"];1387[label="primMinusNat (primDivNatS (primMinusNatS (Succ vuy580) vuy59) (Succ vuy60)) Zero",fontsize=16,color="burlywood",shape="box"];2639[label="vuy59/Succ vuy590",fontsize=10,color="white",style="solid",shape="box"];1387 -> 2639[label="",style="solid", color="burlywood", weight=9];
2639 -> 1402[label="",style="solid", color="burlywood", weight=3];
2640[label="vuy59/Zero",fontsize=10,color="white",style="solid",shape="box"];1387 -> 2640[label="",style="solid", color="burlywood", weight=9];
2640 -> 1403[label="",style="solid", color="burlywood", weight=3];
1388[label="primMinusNat (primDivNatS (primMinusNatS Zero vuy59) (Succ vuy60)) Zero",fontsize=16,color="burlywood",shape="box"];2641[label="vuy59/Succ vuy590",fontsize=10,color="white",style="solid",shape="box"];1388 -> 2641[label="",style="solid", color="burlywood", weight=9];
2641 -> 1404[label="",style="solid", color="burlywood", weight=3];
2642[label="vuy59/Zero",fontsize=10,color="white",style="solid",shape="box"];1388 -> 2642[label="",style="solid", color="burlywood", weight=9];
2642 -> 1405[label="",style="solid", color="burlywood", weight=3];
989[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) (primGEqNatS (Succ vuy530) (Succ vuy540))) (Succ Zero)",fontsize=16,color="black",shape="box"];989 -> 994[label="",style="solid", color="black", weight=3];
990[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) (primGEqNatS (Succ vuy530) Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];990 -> 995[label="",style="solid", color="black", weight=3];
991[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) (primGEqNatS Zero (Succ vuy540))) (Succ Zero)",fontsize=16,color="black",shape="box"];991 -> 996[label="",style="solid", color="black", weight=3];
992[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) (primGEqNatS Zero Zero)) (Succ Zero)",fontsize=16,color="black",shape="box"];992 -> 997[label="",style="solid", color="black", weight=3];
330 -> 1465[label="",style="dashed", color="red", weight=0];
330[label="primPlusNat (primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero)) Zero",fontsize=16,color="magenta"];330 -> 1466[label="",style="dashed", color="magenta", weight=3];
330 -> 1467[label="",style="dashed", color="magenta", weight=3];
330 -> 1468[label="",style="dashed", color="magenta", weight=3];
331 -> 1465[label="",style="dashed", color="red", weight=0];
331[label="primPlusNat (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)) Zero",fontsize=16,color="magenta"];331 -> 1469[label="",style="dashed", color="magenta", weight=3];
331 -> 1470[label="",style="dashed", color="magenta", weight=3];
331 -> 1471[label="",style="dashed", color="magenta", weight=3];
932[label="vuy410",fontsize=16,color="green",shape="box"];933[label="vuy400",fontsize=16,color="green",shape="box"];934[label="primMinusNat (Succ (primDivNatS (primMinusNatS (Succ vuy38) (Succ vuy39)) (Succ (Succ vuy39)))) (Succ Zero)",fontsize=16,color="black",shape="box"];934 -> 988[label="",style="solid", color="black", weight=3];
935 -> 254[label="",style="dashed", color="red", weight=0];
935[label="primMinusNat Zero (Succ Zero)",fontsize=16,color="magenta"];1402[label="primMinusNat (primDivNatS (primMinusNatS (Succ vuy580) (Succ vuy590)) (Succ vuy60)) Zero",fontsize=16,color="black",shape="box"];1402 -> 1421[label="",style="solid", color="black", weight=3];
1403[label="primMinusNat (primDivNatS (primMinusNatS (Succ vuy580) Zero) (Succ vuy60)) Zero",fontsize=16,color="black",shape="box"];1403 -> 1422[label="",style="solid", color="black", weight=3];
1404[label="primMinusNat (primDivNatS (primMinusNatS Zero (Succ vuy590)) (Succ vuy60)) Zero",fontsize=16,color="black",shape="box"];1404 -> 1423[label="",style="solid", color="black", weight=3];
1405[label="primMinusNat (primDivNatS (primMinusNatS Zero Zero) (Succ vuy60)) Zero",fontsize=16,color="black",shape="box"];1405 -> 1424[label="",style="solid", color="black", weight=3];
994 -> 945[label="",style="dashed", color="red", weight=0];
994[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) (primGEqNatS vuy530 vuy540)) (Succ Zero)",fontsize=16,color="magenta"];994 -> 1000[label="",style="dashed", color="magenta", weight=3];
994 -> 1001[label="",style="dashed", color="magenta", weight=3];
995[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) True) (Succ Zero)",fontsize=16,color="black",shape="triangle"];995 -> 1002[label="",style="solid", color="black", weight=3];
996[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) False) (Succ Zero)",fontsize=16,color="black",shape="box"];996 -> 1003[label="",style="solid", color="black", weight=3];
997 -> 995[label="",style="dashed", color="red", weight=0];
997[label="primPlusNat (primDivNatS0 (Succ vuy51) (Succ vuy52) True) (Succ Zero)",fontsize=16,color="magenta"];1466[label="Zero",fontsize=16,color="green",shape="box"];1467[label="Zero",fontsize=16,color="green",shape="box"];1468[label="Succ vuy30000",fontsize=16,color="green",shape="box"];1465[label="primPlusNat (primDivNatS (primMinusNatS vuy64 vuy65) (Succ vuy66)) Zero",fontsize=16,color="burlywood",shape="triangle"];2648[label="vuy64/Succ vuy640",fontsize=10,color="white",style="solid",shape="box"];1465 -> 2648[label="",style="solid", color="burlywood", weight=9];
2648 -> 1499[label="",style="solid", color="burlywood", weight=3];
2649[label="vuy64/Zero",fontsize=10,color="white",style="solid",shape="box"];1465 -> 2649[label="",style="solid", color="burlywood", weight=9];
2649 -> 1500[label="",style="solid", color="burlywood", weight=3];
1469[label="Zero",fontsize=16,color="green",shape="box"];1470[label="Zero",fontsize=16,color="green",shape="box"];1471[label="Zero",fontsize=16,color="green",shape="box"];988 -> 1353[label="",style="dashed", color="red", weight=0];
988[label="primMinusNat (primDivNatS (primMinusNatS (Succ vuy38) (Succ vuy39)) (Succ (Succ vuy39))) Zero",fontsize=16,color="magenta"];988 -> 1360[label="",style="dashed", color="magenta", weight=3];
988 -> 1361[label="",style="dashed", color="magenta", weight=3];
988 -> 1362[label="",style="dashed", color="magenta", weight=3];
1421 -> 1353[label="",style="dashed", color="red", weight=0];
1421[label="primMinusNat (primDivNatS (primMinusNatS vuy580 vuy590) (Succ vuy60)) Zero",fontsize=16,color="magenta"];1421 -> 1440[label="",style="dashed", color="magenta", weight=3];
1421 -> 1441[label="",style="dashed", color="magenta", weight=3];
1422[label="primMinusNat (primDivNatS (Succ vuy580) (Succ vuy60)) Zero",fontsize=16,color="black",shape="box"];1422 -> 1442[label="",style="solid", color="black", weight=3];
1423[label="primMinusNat (primDivNatS Zero (Succ vuy60)) Zero",fontsize=16,color="black",shape="triangle"];1423 -> 1443[label="",style="solid", color="black", weight=3];
1424 -> 1423[label="",style="dashed", color="red", weight=0];
1424[label="primMinusNat (primDivNatS Zero (Succ vuy60)) Zero",fontsize=16,color="magenta"];1000[label="vuy540",fontsize=16,color="green",shape="box"];1001[label="vuy530",fontsize=16,color="green",shape="box"];1002[label="primPlusNat (Succ (primDivNatS (primMinusNatS (Succ vuy51) (Succ vuy52)) (Succ (Succ vuy52)))) (Succ Zero)",fontsize=16,color="black",shape="box"];1002 -> 1008[label="",style="solid", color="black", weight=3];
1003 -> 263[label="",style="dashed", color="red", weight=0];
1003[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="magenta"];1499[label="primPlusNat (primDivNatS (primMinusNatS (Succ vuy640) vuy65) (Succ vuy66)) Zero",fontsize=16,color="burlywood",shape="box"];2654[label="vuy65/Succ vuy650",fontsize=10,color="white",style="solid",shape="box"];1499 -> 2654[label="",style="solid", color="burlywood", weight=9];
2654 -> 1505[label="",style="solid", color="burlywood", weight=3];
2655[label="vuy65/Zero",fontsize=10,color="white",style="solid",shape="box"];1499 -> 2655[label="",style="solid", color="burlywood", weight=9];
2655 -> 1506[label="",style="solid", color="burlywood", weight=3];
1500[label="primPlusNat (primDivNatS (primMinusNatS Zero vuy65) (Succ vuy66)) Zero",fontsize=16,color="burlywood",shape="box"];2656[label="vuy65/Succ vuy650",fontsize=10,color="white",style="solid",shape="box"];1500 -> 2656[label="",style="solid", color="burlywood", weight=9];
2656 -> 1507[label="",style="solid", color="burlywood", weight=3];
2657[label="vuy65/Zero",fontsize=10,color="white",style="solid",shape="box"];1500 -> 2657[label="",style="solid", color="burlywood", weight=9];
2657 -> 1508[label="",style="solid", color="burlywood", weight=3];
1360[label="Succ vuy38",fontsize=16,color="green",shape="box"];1361[label="Succ vuy39",fontsize=16,color="green",shape="box"];1362[label="Succ vuy39",fontsize=16,color="green",shape="box"];1440[label="vuy580",fontsize=16,color="green",shape="box"];1441[label="vuy590",fontsize=16,color="green",shape="box"];1442[label="primMinusNat (primDivNatS0 vuy580 vuy60 (primGEqNatS vuy580 vuy60)) Zero",fontsize=16,color="burlywood",shape="box"];2658[label="vuy580/Succ vuy5800",fontsize=10,color="white",style="solid",shape="box"];1442 -> 2658[label="",style="solid", color="burlywood", weight=9];
2658 -> 1457[label="",style="solid", color="burlywood", weight=3];
2659[label="vuy580/Zero",fontsize=10,color="white",style="solid",shape="box"];1442 -> 2659[label="",style="solid", color="burlywood", weight=9];
2659 -> 1458[label="",style="solid", color="burlywood", weight=3];
1443[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="triangle"];1443 -> 1459[label="",style="solid", color="black", weight=3];
1008[label="Succ (Succ (primPlusNat (primDivNatS (primMinusNatS (Succ vuy51) (Succ vuy52)) (Succ (Succ vuy52))) Zero))",fontsize=16,color="green",shape="box"];1008 -> 1013[label="",style="dashed", color="green", weight=3];
1505[label="primPlusNat (primDivNatS (primMinusNatS (Succ vuy640) (Succ vuy650)) (Succ vuy66)) Zero",fontsize=16,color="black",shape="box"];1505 -> 1513[label="",style="solid", color="black", weight=3];
1506[label="primPlusNat (primDivNatS (primMinusNatS (Succ vuy640) Zero) (Succ vuy66)) Zero",fontsize=16,color="black",shape="box"];1506 -> 1514[label="",style="solid", color="black", weight=3];
1507[label="primPlusNat (primDivNatS (primMinusNatS Zero (Succ vuy650)) (Succ vuy66)) Zero",fontsize=16,color="black",shape="box"];1507 -> 1515[label="",style="solid", color="black", weight=3];
1508[label="primPlusNat (primDivNatS (primMinusNatS Zero Zero) (Succ vuy66)) Zero",fontsize=16,color="black",shape="box"];1508 -> 1516[label="",style="solid", color="black", weight=3];
1457[label="primMinusNat (primDivNatS0 (Succ vuy5800) vuy60 (primGEqNatS (Succ vuy5800) vuy60)) Zero",fontsize=16,color="burlywood",shape="box"];2660[label="vuy60/Succ vuy600",fontsize=10,color="white",style="solid",shape="box"];1457 -> 2660[label="",style="solid", color="burlywood", weight=9];
2660 -> 1501[label="",style="solid", color="burlywood", weight=3];
2661[label="vuy60/Zero",fontsize=10,color="white",style="solid",shape="box"];1457 -> 2661[label="",style="solid", color="burlywood", weight=9];
2661 -> 1502[label="",style="solid", color="burlywood", weight=3];
1458[label="primMinusNat (primDivNatS0 Zero vuy60 (primGEqNatS Zero vuy60)) Zero",fontsize=16,color="burlywood",shape="box"];2662[label="vuy60/Succ vuy600",fontsize=10,color="white",style="solid",shape="box"];1458 -> 2662[label="",style="solid", color="burlywood", weight=9];
2662 -> 1503[label="",style="solid", color="burlywood", weight=3];
2663[label="vuy60/Zero",fontsize=10,color="white",style="solid",shape="box"];1458 -> 2663[label="",style="solid", color="burlywood", weight=9];
2663 -> 1504[label="",style="solid", color="burlywood", weight=3];
1459[label="Pos Zero",fontsize=16,color="green",shape="box"];1013 -> 1465[label="",style="dashed", color="red", weight=0];
1013[label="primPlusNat (primDivNatS (primMinusNatS (Succ vuy51) (Succ vuy52)) (Succ (Succ vuy52))) Zero",fontsize=16,color="magenta"];1013 -> 1472[label="",style="dashed", color="magenta", weight=3];
1013 -> 1473[label="",style="dashed", color="magenta", weight=3];
1013 -> 1474[label="",style="dashed", color="magenta", weight=3];
1513 -> 1465[label="",style="dashed", color="red", weight=0];
1513[label="primPlusNat (primDivNatS (primMinusNatS vuy640 vuy650) (Succ vuy66)) Zero",fontsize=16,color="magenta"];1513 -> 1522[label="",style="dashed", color="magenta", weight=3];
1513 -> 1523[label="",style="dashed", color="magenta", weight=3];
1514[label="primPlusNat (primDivNatS (Succ vuy640) (Succ vuy66)) Zero",fontsize=16,color="black",shape="box"];1514 -> 1524[label="",style="solid", color="black", weight=3];
1515[label="primPlusNat (primDivNatS Zero (Succ vuy66)) Zero",fontsize=16,color="black",shape="triangle"];1515 -> 1525[label="",style="solid", color="black", weight=3];
1516 -> 1515[label="",style="dashed", color="red", weight=0];
1516[label="primPlusNat (primDivNatS Zero (Succ vuy66)) Zero",fontsize=16,color="magenta"];1501[label="primMinusNat (primDivNatS0 (Succ vuy5800) (Succ vuy600) (primGEqNatS (Succ vuy5800) (Succ vuy600))) Zero",fontsize=16,color="black",shape="box"];1501 -> 1509[label="",style="solid", color="black", weight=3];
1502[label="primMinusNat (primDivNatS0 (Succ vuy5800) Zero (primGEqNatS (Succ vuy5800) Zero)) Zero",fontsize=16,color="black",shape="box"];1502 -> 1510[label="",style="solid", color="black", weight=3];
1503[label="primMinusNat (primDivNatS0 Zero (Succ vuy600) (primGEqNatS Zero (Succ vuy600))) Zero",fontsize=16,color="black",shape="box"];1503 -> 1511[label="",style="solid", color="black", weight=3];
1504[label="primMinusNat (primDivNatS0 Zero Zero (primGEqNatS Zero Zero)) Zero",fontsize=16,color="black",shape="box"];1504 -> 1512[label="",style="solid", color="black", weight=3];
1472[label="Succ vuy52",fontsize=16,color="green",shape="box"];1473[label="Succ vuy52",fontsize=16,color="green",shape="box"];1474[label="Succ vuy51",fontsize=16,color="green",shape="box"];1522[label="vuy650",fontsize=16,color="green",shape="box"];1523[label="vuy640",fontsize=16,color="green",shape="box"];1524[label="primPlusNat (primDivNatS0 vuy640 vuy66 (primGEqNatS vuy640 vuy66)) Zero",fontsize=16,color="burlywood",shape="box"];2667[label="vuy640/Succ vuy6400",fontsize=10,color="white",style="solid",shape="box"];1524 -> 2667[label="",style="solid", color="burlywood", weight=9];
2667 -> 1532[label="",style="solid", color="burlywood", weight=3];
2668[label="vuy640/Zero",fontsize=10,color="white",style="solid",shape="box"];1524 -> 2668[label="",style="solid", color="burlywood", weight=9];
2668 -> 1533[label="",style="solid", color="burlywood", weight=3];
1525[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="triangle"];1525 -> 1534[label="",style="solid", color="black", weight=3];
1509 -> 2028[label="",style="dashed", color="red", weight=0];
1509[label="primMinusNat (primDivNatS0 (Succ vuy5800) (Succ vuy600) (primGEqNatS vuy5800 vuy600)) Zero",fontsize=16,color="magenta"];1509 -> 2029[label="",style="dashed", color="magenta", weight=3];
1509 -> 2030[label="",style="dashed", color="magenta", weight=3];
1509 -> 2031[label="",style="dashed", color="magenta", weight=3];
1509 -> 2032[label="",style="dashed", color="magenta", weight=3];
1510[label="primMinusNat (primDivNatS0 (Succ vuy5800) Zero True) Zero",fontsize=16,color="black",shape="box"];1510 -> 1519[label="",style="solid", color="black", weight=3];
1511[label="primMinusNat (primDivNatS0 Zero (Succ vuy600) False) Zero",fontsize=16,color="black",shape="box"];1511 -> 1520[label="",style="solid", color="black", weight=3];
1512[label="primMinusNat (primDivNatS0 Zero Zero True) Zero",fontsize=16,color="black",shape="box"];1512 -> 1521[label="",style="solid", color="black", weight=3];
1532[label="primPlusNat (primDivNatS0 (Succ vuy6400) vuy66 (primGEqNatS (Succ vuy6400) vuy66)) Zero",fontsize=16,color="burlywood",shape="box"];2670[label="vuy66/Succ vuy660",fontsize=10,color="white",style="solid",shape="box"];1532 -> 2670[label="",style="solid", color="burlywood", weight=9];
2670 -> 1541[label="",style="solid", color="burlywood", weight=3];
2671[label="vuy66/Zero",fontsize=10,color="white",style="solid",shape="box"];1532 -> 2671[label="",style="solid", color="burlywood", weight=9];
2671 -> 1542[label="",style="solid", color="burlywood", weight=3];
1533[label="primPlusNat (primDivNatS0 Zero vuy66 (primGEqNatS Zero vuy66)) Zero",fontsize=16,color="burlywood",shape="box"];2672[label="vuy66/Succ vuy660",fontsize=10,color="white",style="solid",shape="box"];1533 -> 2672[label="",style="solid", color="burlywood", weight=9];
2672 -> 1543[label="",style="solid", color="burlywood", weight=3];
2673[label="vuy66/Zero",fontsize=10,color="white",style="solid",shape="box"];1533 -> 2673[label="",style="solid", color="burlywood", weight=9];
2673 -> 1544[label="",style="solid", color="burlywood", weight=3];
1534[label="Zero",fontsize=16,color="green",shape="box"];2029[label="vuy5800",fontsize=16,color="green",shape="box"];2030[label="vuy600",fontsize=16,color="green",shape="box"];2031[label="vuy600",fontsize=16,color="green",shape="box"];2032[label="vuy5800",fontsize=16,color="green",shape="box"];2028[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) (primGEqNatS vuy97 vuy98)) Zero",fontsize=16,color="burlywood",shape="triangle"];2674[label="vuy97/Succ vuy970",fontsize=10,color="white",style="solid",shape="box"];2028 -> 2674[label="",style="solid", color="burlywood", weight=9];
2674 -> 2069[label="",style="solid", color="burlywood", weight=3];
2675[label="vuy97/Zero",fontsize=10,color="white",style="solid",shape="box"];2028 -> 2675[label="",style="solid", color="burlywood", weight=9];
2675 -> 2070[label="",style="solid", color="burlywood", weight=3];
1519 -> 1874[label="",style="dashed", color="red", weight=0];
1519[label="primMinusNat (Succ (primDivNatS (primMinusNatS (Succ vuy5800) Zero) (Succ Zero))) Zero",fontsize=16,color="magenta"];1519 -> 1875[label="",style="dashed", color="magenta", weight=3];
1520 -> 1443[label="",style="dashed", color="red", weight=0];
1520[label="primMinusNat Zero Zero",fontsize=16,color="magenta"];1521 -> 1874[label="",style="dashed", color="red", weight=0];
1521[label="primMinusNat (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))) Zero",fontsize=16,color="magenta"];1521 -> 1876[label="",style="dashed", color="magenta", weight=3];
1541[label="primPlusNat (primDivNatS0 (Succ vuy6400) (Succ vuy660) (primGEqNatS (Succ vuy6400) (Succ vuy660))) Zero",fontsize=16,color="black",shape="box"];1541 -> 1552[label="",style="solid", color="black", weight=3];
1542[label="primPlusNat (primDivNatS0 (Succ vuy6400) Zero (primGEqNatS (Succ vuy6400) Zero)) Zero",fontsize=16,color="black",shape="box"];1542 -> 1553[label="",style="solid", color="black", weight=3];
1543[label="primPlusNat (primDivNatS0 Zero (Succ vuy660) (primGEqNatS Zero (Succ vuy660))) Zero",fontsize=16,color="black",shape="box"];1543 -> 1554[label="",style="solid", color="black", weight=3];
1544[label="primPlusNat (primDivNatS0 Zero Zero (primGEqNatS Zero Zero)) Zero",fontsize=16,color="black",shape="box"];1544 -> 1555[label="",style="solid", color="black", weight=3];
2069[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) (primGEqNatS (Succ vuy970) vuy98)) Zero",fontsize=16,color="burlywood",shape="box"];2679[label="vuy98/Succ vuy980",fontsize=10,color="white",style="solid",shape="box"];2069 -> 2679[label="",style="solid", color="burlywood", weight=9];
2679 -> 2084[label="",style="solid", color="burlywood", weight=3];
2680[label="vuy98/Zero",fontsize=10,color="white",style="solid",shape="box"];2069 -> 2680[label="",style="solid", color="burlywood", weight=9];
2680 -> 2085[label="",style="solid", color="burlywood", weight=3];
2070[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) (primGEqNatS Zero vuy98)) Zero",fontsize=16,color="burlywood",shape="box"];2681[label="vuy98/Succ vuy980",fontsize=10,color="white",style="solid",shape="box"];2070 -> 2681[label="",style="solid", color="burlywood", weight=9];
2681 -> 2086[label="",style="solid", color="burlywood", weight=3];
2682[label="vuy98/Zero",fontsize=10,color="white",style="solid",shape="box"];2070 -> 2682[label="",style="solid", color="burlywood", weight=9];
2682 -> 2087[label="",style="solid", color="burlywood", weight=3];
1875 -> 2256[label="",style="dashed", color="red", weight=0];
1875[label="primDivNatS (primMinusNatS (Succ vuy5800) Zero) (Succ Zero)",fontsize=16,color="magenta"];1875 -> 2257[label="",style="dashed", color="magenta", weight=3];
1875 -> 2258[label="",style="dashed", color="magenta", weight=3];
1875 -> 2259[label="",style="dashed", color="magenta", weight=3];
1874[label="primMinusNat (Succ vuy79) Zero",fontsize=16,color="black",shape="triangle"];1874 -> 1890[label="",style="solid", color="black", weight=3];
1876 -> 2256[label="",style="dashed", color="red", weight=0];
1876[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];1876 -> 2260[label="",style="dashed", color="magenta", weight=3];
1876 -> 2261[label="",style="dashed", color="magenta", weight=3];
1876 -> 2262[label="",style="dashed", color="magenta", weight=3];
1552 -> 2161[label="",style="dashed", color="red", weight=0];
1552[label="primPlusNat (primDivNatS0 (Succ vuy6400) (Succ vuy660) (primGEqNatS vuy6400 vuy660)) Zero",fontsize=16,color="magenta"];1552 -> 2162[label="",style="dashed", color="magenta", weight=3];
1552 -> 2163[label="",style="dashed", color="magenta", weight=3];
1552 -> 2164[label="",style="dashed", color="magenta", weight=3];
1552 -> 2165[label="",style="dashed", color="magenta", weight=3];
1553[label="primPlusNat (primDivNatS0 (Succ vuy6400) Zero True) Zero",fontsize=16,color="black",shape="box"];1553 -> 1566[label="",style="solid", color="black", weight=3];
1554[label="primPlusNat (primDivNatS0 Zero (Succ vuy660) False) Zero",fontsize=16,color="black",shape="box"];1554 -> 1567[label="",style="solid", color="black", weight=3];
1555[label="primPlusNat (primDivNatS0 Zero Zero True) Zero",fontsize=16,color="black",shape="box"];1555 -> 1568[label="",style="solid", color="black", weight=3];
2084[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) (primGEqNatS (Succ vuy970) (Succ vuy980))) Zero",fontsize=16,color="black",shape="box"];2084 -> 2102[label="",style="solid", color="black", weight=3];
2085[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) (primGEqNatS (Succ vuy970) Zero)) Zero",fontsize=16,color="black",shape="box"];2085 -> 2103[label="",style="solid", color="black", weight=3];
2086[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) (primGEqNatS Zero (Succ vuy980))) Zero",fontsize=16,color="black",shape="box"];2086 -> 2104[label="",style="solid", color="black", weight=3];
2087[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) (primGEqNatS Zero Zero)) Zero",fontsize=16,color="black",shape="box"];2087 -> 2105[label="",style="solid", color="black", weight=3];
2257[label="Succ vuy5800",fontsize=16,color="green",shape="box"];2258[label="Zero",fontsize=16,color="green",shape="box"];2259[label="Zero",fontsize=16,color="green",shape="box"];2256[label="primDivNatS (primMinusNatS vuy116 vuy117) (Succ vuy118)",fontsize=16,color="burlywood",shape="triangle"];2686[label="vuy116/Succ vuy1160",fontsize=10,color="white",style="solid",shape="box"];2256 -> 2686[label="",style="solid", color="burlywood", weight=9];
2686 -> 2308[label="",style="solid", color="burlywood", weight=3];
2687[label="vuy116/Zero",fontsize=10,color="white",style="solid",shape="box"];2256 -> 2687[label="",style="solid", color="burlywood", weight=9];
2687 -> 2309[label="",style="solid", color="burlywood", weight=3];
1890[label="Pos (Succ vuy79)",fontsize=16,color="green",shape="box"];2260[label="Zero",fontsize=16,color="green",shape="box"];2261[label="Zero",fontsize=16,color="green",shape="box"];2262[label="Zero",fontsize=16,color="green",shape="box"];2162[label="vuy6400",fontsize=16,color="green",shape="box"];2163[label="vuy6400",fontsize=16,color="green",shape="box"];2164[label="vuy660",fontsize=16,color="green",shape="box"];2165[label="vuy660",fontsize=16,color="green",shape="box"];2161[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) (primGEqNatS vuy113 vuy114)) Zero",fontsize=16,color="burlywood",shape="triangle"];2688[label="vuy113/Succ vuy1130",fontsize=10,color="white",style="solid",shape="box"];2161 -> 2688[label="",style="solid", color="burlywood", weight=9];
2688 -> 2202[label="",style="solid", color="burlywood", weight=3];
2689[label="vuy113/Zero",fontsize=10,color="white",style="solid",shape="box"];2161 -> 2689[label="",style="solid", color="burlywood", weight=9];
2689 -> 2203[label="",style="solid", color="burlywood", weight=3];
1566 -> 1581[label="",style="dashed", color="red", weight=0];
1566[label="primPlusNat (Succ (primDivNatS (primMinusNatS (Succ vuy6400) Zero) (Succ Zero))) Zero",fontsize=16,color="magenta"];1566 -> 1582[label="",style="dashed", color="magenta", weight=3];
1567 -> 1525[label="",style="dashed", color="red", weight=0];
1567[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];1568 -> 1581[label="",style="dashed", color="red", weight=0];
1568[label="primPlusNat (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))) Zero",fontsize=16,color="magenta"];1568 -> 1583[label="",style="dashed", color="magenta", weight=3];
2102 -> 2028[label="",style="dashed", color="red", weight=0];
2102[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) (primGEqNatS vuy970 vuy980)) Zero",fontsize=16,color="magenta"];2102 -> 2121[label="",style="dashed", color="magenta", weight=3];
2102 -> 2122[label="",style="dashed", color="magenta", weight=3];
2103[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) True) Zero",fontsize=16,color="black",shape="triangle"];2103 -> 2123[label="",style="solid", color="black", weight=3];
2104[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) False) Zero",fontsize=16,color="black",shape="box"];2104 -> 2124[label="",style="solid", color="black", weight=3];
2105 -> 2103[label="",style="dashed", color="red", weight=0];
2105[label="primMinusNat (primDivNatS0 (Succ vuy95) (Succ vuy96) True) Zero",fontsize=16,color="magenta"];2308[label="primDivNatS (primMinusNatS (Succ vuy1160) vuy117) (Succ vuy118)",fontsize=16,color="burlywood",shape="box"];2695[label="vuy117/Succ vuy1170",fontsize=10,color="white",style="solid",shape="box"];2308 -> 2695[label="",style="solid", color="burlywood", weight=9];
2695 -> 2310[label="",style="solid", color="burlywood", weight=3];
2696[label="vuy117/Zero",fontsize=10,color="white",style="solid",shape="box"];2308 -> 2696[label="",style="solid", color="burlywood", weight=9];
2696 -> 2311[label="",style="solid", color="burlywood", weight=3];
2309[label="primDivNatS (primMinusNatS Zero vuy117) (Succ vuy118)",fontsize=16,color="burlywood",shape="box"];2697[label="vuy117/Succ vuy1170",fontsize=10,color="white",style="solid",shape="box"];2309 -> 2697[label="",style="solid", color="burlywood", weight=9];
2697 -> 2312[label="",style="solid", color="burlywood", weight=3];
2698[label="vuy117/Zero",fontsize=10,color="white",style="solid",shape="box"];2309 -> 2698[label="",style="solid", color="burlywood", weight=9];
2698 -> 2313[label="",style="solid", color="burlywood", weight=3];
2202[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) (primGEqNatS (Succ vuy1130) vuy114)) Zero",fontsize=16,color="burlywood",shape="box"];2699[label="vuy114/Succ vuy1140",fontsize=10,color="white",style="solid",shape="box"];2202 -> 2699[label="",style="solid", color="burlywood", weight=9];
2699 -> 2210[label="",style="solid", color="burlywood", weight=3];
2700[label="vuy114/Zero",fontsize=10,color="white",style="solid",shape="box"];2202 -> 2700[label="",style="solid", color="burlywood", weight=9];
2700 -> 2211[label="",style="solid", color="burlywood", weight=3];
2203[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) (primGEqNatS Zero vuy114)) Zero",fontsize=16,color="burlywood",shape="box"];2701[label="vuy114/Succ vuy1140",fontsize=10,color="white",style="solid",shape="box"];2203 -> 2701[label="",style="solid", color="burlywood", weight=9];
2701 -> 2212[label="",style="solid", color="burlywood", weight=3];
2702[label="vuy114/Zero",fontsize=10,color="white",style="solid",shape="box"];2203 -> 2702[label="",style="solid", color="burlywood", weight=9];
2702 -> 2213[label="",style="solid", color="burlywood", weight=3];
1582 -> 2256[label="",style="dashed", color="red", weight=0];
1582[label="primDivNatS (primMinusNatS (Succ vuy6400) Zero) (Succ Zero)",fontsize=16,color="magenta"];1582 -> 2269[label="",style="dashed", color="magenta", weight=3];
1582 -> 2270[label="",style="dashed", color="magenta", weight=3];
1582 -> 2271[label="",style="dashed", color="magenta", weight=3];
1581[label="primPlusNat (Succ vuy67) Zero",fontsize=16,color="black",shape="triangle"];1581 -> 1589[label="",style="solid", color="black", weight=3];
1583 -> 2256[label="",style="dashed", color="red", weight=0];
1583[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];1583 -> 2272[label="",style="dashed", color="magenta", weight=3];
1583 -> 2273[label="",style="dashed", color="magenta", weight=3];
1583 -> 2274[label="",style="dashed", color="magenta", weight=3];
2121[label="vuy970",fontsize=16,color="green",shape="box"];2122[label="vuy980",fontsize=16,color="green",shape="box"];2123 -> 1874[label="",style="dashed", color="red", weight=0];
2123[label="primMinusNat (Succ (primDivNatS (primMinusNatS (Succ vuy95) (Succ vuy96)) (Succ (Succ vuy96)))) Zero",fontsize=16,color="magenta"];2123 -> 2136[label="",style="dashed", color="magenta", weight=3];
2124 -> 1443[label="",style="dashed", color="red", weight=0];
2124[label="primMinusNat Zero Zero",fontsize=16,color="magenta"];2310[label="primDivNatS (primMinusNatS (Succ vuy1160) (Succ vuy1170)) (Succ vuy118)",fontsize=16,color="black",shape="box"];2310 -> 2314[label="",style="solid", color="black", weight=3];
2311[label="primDivNatS (primMinusNatS (Succ vuy1160) Zero) (Succ vuy118)",fontsize=16,color="black",shape="box"];2311 -> 2315[label="",style="solid", color="black", weight=3];
2312[label="primDivNatS (primMinusNatS Zero (Succ vuy1170)) (Succ vuy118)",fontsize=16,color="black",shape="box"];2312 -> 2316[label="",style="solid", color="black", weight=3];
2313[label="primDivNatS (primMinusNatS Zero Zero) (Succ vuy118)",fontsize=16,color="black",shape="box"];2313 -> 2317[label="",style="solid", color="black", weight=3];
2210[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) (primGEqNatS (Succ vuy1130) (Succ vuy1140))) Zero",fontsize=16,color="black",shape="box"];2210 -> 2224[label="",style="solid", color="black", weight=3];
2211[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) (primGEqNatS (Succ vuy1130) Zero)) Zero",fontsize=16,color="black",shape="box"];2211 -> 2225[label="",style="solid", color="black", weight=3];
2212[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) (primGEqNatS Zero (Succ vuy1140))) Zero",fontsize=16,color="black",shape="box"];2212 -> 2226[label="",style="solid", color="black", weight=3];
2213[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) (primGEqNatS Zero Zero)) Zero",fontsize=16,color="black",shape="box"];2213 -> 2227[label="",style="solid", color="black", weight=3];
2269[label="Succ vuy6400",fontsize=16,color="green",shape="box"];2270[label="Zero",fontsize=16,color="green",shape="box"];2271[label="Zero",fontsize=16,color="green",shape="box"];1589[label="Succ vuy67",fontsize=16,color="green",shape="box"];2272[label="Zero",fontsize=16,color="green",shape="box"];2273[label="Zero",fontsize=16,color="green",shape="box"];2274[label="Zero",fontsize=16,color="green",shape="box"];2136 -> 2256[label="",style="dashed", color="red", weight=0];
2136[label="primDivNatS (primMinusNatS (Succ vuy95) (Succ vuy96)) (Succ (Succ vuy96))",fontsize=16,color="magenta"];2136 -> 2278[label="",style="dashed", color="magenta", weight=3];
2136 -> 2279[label="",style="dashed", color="magenta", weight=3];
2136 -> 2280[label="",style="dashed", color="magenta", weight=3];
2314 -> 2256[label="",style="dashed", color="red", weight=0];
2314[label="primDivNatS (primMinusNatS vuy1160 vuy1170) (Succ vuy118)",fontsize=16,color="magenta"];2314 -> 2318[label="",style="dashed", color="magenta", weight=3];
2314 -> 2319[label="",style="dashed", color="magenta", weight=3];
2315[label="primDivNatS (Succ vuy1160) (Succ vuy118)",fontsize=16,color="black",shape="box"];2315 -> 2320[label="",style="solid", color="black", weight=3];
2316[label="primDivNatS Zero (Succ vuy118)",fontsize=16,color="black",shape="triangle"];2316 -> 2321[label="",style="solid", color="black", weight=3];
2317 -> 2316[label="",style="dashed", color="red", weight=0];
2317[label="primDivNatS Zero (Succ vuy118)",fontsize=16,color="magenta"];2224 -> 2161[label="",style="dashed", color="red", weight=0];
2224[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) (primGEqNatS vuy1130 vuy1140)) Zero",fontsize=16,color="magenta"];2224 -> 2236[label="",style="dashed", color="magenta", weight=3];
2224 -> 2237[label="",style="dashed", color="magenta", weight=3];
2225[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) True) Zero",fontsize=16,color="black",shape="triangle"];2225 -> 2238[label="",style="solid", color="black", weight=3];
2226[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) False) Zero",fontsize=16,color="black",shape="box"];2226 -> 2239[label="",style="solid", color="black", weight=3];
2227 -> 2225[label="",style="dashed", color="red", weight=0];
2227[label="primPlusNat (primDivNatS0 (Succ vuy111) (Succ vuy112) True) Zero",fontsize=16,color="magenta"];2278[label="Succ vuy95",fontsize=16,color="green",shape="box"];2279[label="Succ vuy96",fontsize=16,color="green",shape="box"];2280[label="Succ vuy96",fontsize=16,color="green",shape="box"];2318[label="vuy1160",fontsize=16,color="green",shape="box"];2319[label="vuy1170",fontsize=16,color="green",shape="box"];2320[label="primDivNatS0 vuy1160 vuy118 (primGEqNatS vuy1160 vuy118)",fontsize=16,color="burlywood",shape="box"];2712[label="vuy1160/Succ vuy11600",fontsize=10,color="white",style="solid",shape="box"];2320 -> 2712[label="",style="solid", color="burlywood", weight=9];
2712 -> 2322[label="",style="solid", color="burlywood", weight=3];
2713[label="vuy1160/Zero",fontsize=10,color="white",style="solid",shape="box"];2320 -> 2713[label="",style="solid", color="burlywood", weight=9];
2713 -> 2323[label="",style="solid", color="burlywood", weight=3];
2321[label="Zero",fontsize=16,color="green",shape="box"];2236[label="vuy1130",fontsize=16,color="green",shape="box"];2237[label="vuy1140",fontsize=16,color="green",shape="box"];2238 -> 1581[label="",style="dashed", color="red", weight=0];
2238[label="primPlusNat (Succ (primDivNatS (primMinusNatS (Succ vuy111) (Succ vuy112)) (Succ (Succ vuy112)))) Zero",fontsize=16,color="magenta"];2238 -> 2249[label="",style="dashed", color="magenta", weight=3];
2239 -> 1525[label="",style="dashed", color="red", weight=0];
2239[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];2322[label="primDivNatS0 (Succ vuy11600) vuy118 (primGEqNatS (Succ vuy11600) vuy118)",fontsize=16,color="burlywood",shape="box"];2716[label="vuy118/Succ vuy1180",fontsize=10,color="white",style="solid",shape="box"];2322 -> 2716[label="",style="solid", color="burlywood", weight=9];
2716 -> 2324[label="",style="solid", color="burlywood", weight=3];
2717[label="vuy118/Zero",fontsize=10,color="white",style="solid",shape="box"];2322 -> 2717[label="",style="solid", color="burlywood", weight=9];
2717 -> 2325[label="",style="solid", color="burlywood", weight=3];
2323[label="primDivNatS0 Zero vuy118 (primGEqNatS Zero vuy118)",fontsize=16,color="burlywood",shape="box"];2718[label="vuy118/Succ vuy1180",fontsize=10,color="white",style="solid",shape="box"];2323 -> 2718[label="",style="solid", color="burlywood", weight=9];
2718 -> 2326[label="",style="solid", color="burlywood", weight=3];
2719[label="vuy118/Zero",fontsize=10,color="white",style="solid",shape="box"];2323 -> 2719[label="",style="solid", color="burlywood", weight=9];
2719 -> 2327[label="",style="solid", color="burlywood", weight=3];
2249 -> 2256[label="",style="dashed", color="red", weight=0];
2249[label="primDivNatS (primMinusNatS (Succ vuy111) (Succ vuy112)) (Succ (Succ vuy112))",fontsize=16,color="magenta"];2249 -> 2284[label="",style="dashed", color="magenta", weight=3];
2249 -> 2285[label="",style="dashed", color="magenta", weight=3];
2249 -> 2286[label="",style="dashed", color="magenta", weight=3];
2324[label="primDivNatS0 (Succ vuy11600) (Succ vuy1180) (primGEqNatS (Succ vuy11600) (Succ vuy1180))",fontsize=16,color="black",shape="box"];2324 -> 2328[label="",style="solid", color="black", weight=3];
2325[label="primDivNatS0 (Succ vuy11600) Zero (primGEqNatS (Succ vuy11600) Zero)",fontsize=16,color="black",shape="box"];2325 -> 2329[label="",style="solid", color="black", weight=3];
2326[label="primDivNatS0 Zero (Succ vuy1180) (primGEqNatS Zero (Succ vuy1180))",fontsize=16,color="black",shape="box"];2326 -> 2330[label="",style="solid", color="black", weight=3];
2327[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];2327 -> 2331[label="",style="solid", color="black", weight=3];
2284[label="Succ vuy111",fontsize=16,color="green",shape="box"];2285[label="Succ vuy112",fontsize=16,color="green",shape="box"];2286[label="Succ vuy112",fontsize=16,color="green",shape="box"];2328 -> 2490[label="",style="dashed", color="red", weight=0];
2328[label="primDivNatS0 (Succ vuy11600) (Succ vuy1180) (primGEqNatS vuy11600 vuy1180)",fontsize=16,color="magenta"];2328 -> 2491[label="",style="dashed", color="magenta", weight=3];
2328 -> 2492[label="",style="dashed", color="magenta", weight=3];
2328 -> 2493[label="",style="dashed", color="magenta", weight=3];
2328 -> 2494[label="",style="dashed", color="magenta", weight=3];
2329[label="primDivNatS0 (Succ vuy11600) Zero True",fontsize=16,color="black",shape="box"];2329 -> 2334[label="",style="solid", color="black", weight=3];
2330[label="primDivNatS0 Zero (Succ vuy1180) False",fontsize=16,color="black",shape="box"];2330 -> 2335[label="",style="solid", color="black", weight=3];
2331[label="primDivNatS0 Zero Zero True",fontsize=16,color="black",shape="box"];2331 -> 2336[label="",style="solid", color="black", weight=3];
2491[label="vuy1180",fontsize=16,color="green",shape="box"];2492[label="vuy11600",fontsize=16,color="green",shape="box"];2493[label="vuy1180",fontsize=16,color="green",shape="box"];2494[label="vuy11600",fontsize=16,color="green",shape="box"];2490[label="primDivNatS0 (Succ vuy135) (Succ vuy136) (primGEqNatS vuy137 vuy138)",fontsize=16,color="burlywood",shape="triangle"];2722[label="vuy137/Succ vuy1370",fontsize=10,color="white",style="solid",shape="box"];2490 -> 2722[label="",style="solid", color="burlywood", weight=9];
2722 -> 2523[label="",style="solid", color="burlywood", weight=3];
2723[label="vuy137/Zero",fontsize=10,color="white",style="solid",shape="box"];2490 -> 2723[label="",style="solid", color="burlywood", weight=9];
2723 -> 2524[label="",style="solid", color="burlywood", weight=3];
2334[label="Succ (primDivNatS (primMinusNatS (Succ vuy11600) Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];2334 -> 2341[label="",style="dashed", color="green", weight=3];
2335[label="Zero",fontsize=16,color="green",shape="box"];2336[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];2336 -> 2342[label="",style="dashed", color="green", weight=3];
2523[label="primDivNatS0 (Succ vuy135) (Succ vuy136) (primGEqNatS (Succ vuy1370) vuy138)",fontsize=16,color="burlywood",shape="box"];2724[label="vuy138/Succ vuy1380",fontsize=10,color="white",style="solid",shape="box"];2523 -> 2724[label="",style="solid", color="burlywood", weight=9];
2724 -> 2525[label="",style="solid", color="burlywood", weight=3];
2725[label="vuy138/Zero",fontsize=10,color="white",style="solid",shape="box"];2523 -> 2725[label="",style="solid", color="burlywood", weight=9];
2725 -> 2526[label="",style="solid", color="burlywood", weight=3];
2524[label="primDivNatS0 (Succ vuy135) (Succ vuy136) (primGEqNatS Zero vuy138)",fontsize=16,color="burlywood",shape="box"];2726[label="vuy138/Succ vuy1380",fontsize=10,color="white",style="solid",shape="box"];2524 -> 2726[label="",style="solid", color="burlywood", weight=9];
2726 -> 2527[label="",style="solid", color="burlywood", weight=3];
2727[label="vuy138/Zero",fontsize=10,color="white",style="solid",shape="box"];2524 -> 2727[label="",style="solid", color="burlywood", weight=9];
2727 -> 2528[label="",style="solid", color="burlywood", weight=3];
2341 -> 2256[label="",style="dashed", color="red", weight=0];
2341[label="primDivNatS (primMinusNatS (Succ vuy11600) Zero) (Succ Zero)",fontsize=16,color="magenta"];2341 -> 2347[label="",style="dashed", color="magenta", weight=3];
2341 -> 2348[label="",style="dashed", color="magenta", weight=3];
2341 -> 2349[label="",style="dashed", color="magenta", weight=3];
2342 -> 2256[label="",style="dashed", color="red", weight=0];
2342[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];2342 -> 2350[label="",style="dashed", color="magenta", weight=3];
2342 -> 2351[label="",style="dashed", color="magenta", weight=3];
2342 -> 2352[label="",style="dashed", color="magenta", weight=3];
2525[label="primDivNatS0 (Succ vuy135) (Succ vuy136) (primGEqNatS (Succ vuy1370) (Succ vuy1380))",fontsize=16,color="black",shape="box"];2525 -> 2529[label="",style="solid", color="black", weight=3];
2526[label="primDivNatS0 (Succ vuy135) (Succ vuy136) (primGEqNatS (Succ vuy1370) Zero)",fontsize=16,color="black",shape="box"];2526 -> 2530[label="",style="solid", color="black", weight=3];
2527[label="primDivNatS0 (Succ vuy135) (Succ vuy136) (primGEqNatS Zero (Succ vuy1380))",fontsize=16,color="black",shape="box"];2527 -> 2531[label="",style="solid", color="black", weight=3];
2528[label="primDivNatS0 (Succ vuy135) (Succ vuy136) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];2528 -> 2532[label="",style="solid", color="black", weight=3];
2347[label="Succ vuy11600",fontsize=16,color="green",shape="box"];2348[label="Zero",fontsize=16,color="green",shape="box"];2349[label="Zero",fontsize=16,color="green",shape="box"];2350[label="Zero",fontsize=16,color="green",shape="box"];2351[label="Zero",fontsize=16,color="green",shape="box"];2352[label="Zero",fontsize=16,color="green",shape="box"];2529 -> 2490[label="",style="dashed", color="red", weight=0];
2529[label="primDivNatS0 (Succ vuy135) (Succ vuy136) (primGEqNatS vuy1370 vuy1380)",fontsize=16,color="magenta"];2529 -> 2533[label="",style="dashed", color="magenta", weight=3];
2529 -> 2534[label="",style="dashed", color="magenta", weight=3];
2530[label="primDivNatS0 (Succ vuy135) (Succ vuy136) True",fontsize=16,color="black",shape="triangle"];2530 -> 2535[label="",style="solid", color="black", weight=3];
2531[label="primDivNatS0 (Succ vuy135) (Succ vuy136) False",fontsize=16,color="black",shape="box"];2531 -> 2536[label="",style="solid", color="black", weight=3];
2532 -> 2530[label="",style="dashed", color="red", weight=0];
2532[label="primDivNatS0 (Succ vuy135) (Succ vuy136) True",fontsize=16,color="magenta"];2533[label="vuy1370",fontsize=16,color="green",shape="box"];2534[label="vuy1380",fontsize=16,color="green",shape="box"];2535[label="Succ (primDivNatS (primMinusNatS (Succ vuy135) (Succ vuy136)) (Succ (Succ vuy136)))",fontsize=16,color="green",shape="box"];2535 -> 2537[label="",style="dashed", color="green", weight=3];
2536[label="Zero",fontsize=16,color="green",shape="box"];2537 -> 2256[label="",style="dashed", color="red", weight=0];
2537[label="primDivNatS (primMinusNatS (Succ vuy135) (Succ vuy136)) (Succ (Succ vuy136))",fontsize=16,color="magenta"];2537 -> 2538[label="",style="dashed", color="magenta", weight=3];
2537 -> 2539[label="",style="dashed", color="magenta", weight=3];
2537 -> 2540[label="",style="dashed", color="magenta", weight=3];
2538[label="Succ vuy135",fontsize=16,color="green",shape="box"];2539[label="Succ vuy136",fontsize=16,color="green",shape="box"];2540[label="Succ vuy136",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy135, vuy136, Zero, Zero) → new_primDivNatS00(vuy135, vuy136)
new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Succ(vuy1380)) → new_primDivNatS0(vuy135, vuy136, vuy1370, vuy1380)
new_primDivNatS(Succ(vuy1160), Succ(vuy1170), vuy118) → new_primDivNatS(vuy1160, vuy1170, vuy118)
new_primDivNatS(Succ(Succ(vuy11600)), Zero, Succ(vuy1180)) → new_primDivNatS0(vuy11600, vuy1180, vuy11600, vuy1180)
new_primDivNatS(Succ(Zero), Zero, Zero) → new_primDivNatS(Zero, Zero, Zero)
new_primDivNatS(Succ(Succ(vuy11600)), Zero, Zero) → new_primDivNatS(Succ(vuy11600), Zero, Zero)
new_primDivNatS00(vuy135, vuy136) → new_primDivNatS(Succ(vuy135), Succ(vuy136), Succ(vuy136))
new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Zero) → new_primDivNatS(Succ(vuy135), Succ(vuy136), Succ(vuy136))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ QDPSizeChangeProof

                                    ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuy11600)), Zero, Zero) → new_primDivNatS(Succ(vuy11600), Zero, Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS(Succ(Succ(vuy11600)), Zero, Zero) → new_primDivNatS(Succ(vuy11600), Zero, Zero)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 2, 2 >= 3, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ QDPOrderProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy135, vuy136, Zero, Zero) → new_primDivNatS00(vuy135, vuy136)
new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Succ(vuy1380)) → new_primDivNatS0(vuy135, vuy136, vuy1370, vuy1380)
new_primDivNatS(Succ(vuy1160), Succ(vuy1170), vuy118) → new_primDivNatS(vuy1160, vuy1170, vuy118)
new_primDivNatS(Succ(Succ(vuy11600)), Zero, Succ(vuy1180)) → new_primDivNatS0(vuy11600, vuy1180, vuy11600, vuy1180)
new_primDivNatS00(vuy135, vuy136) → new_primDivNatS(Succ(vuy135), Succ(vuy136), Succ(vuy136))
new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Zero) → new_primDivNatS(Succ(vuy135), Succ(vuy136), Succ(vuy136))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primDivNatS(Succ(vuy1160), Succ(vuy1170), vuy118) → new_primDivNatS(vuy1160, vuy1170, vuy118)
new_primDivNatS(Succ(Succ(vuy11600)), Zero, Succ(vuy1180)) → new_primDivNatS0(vuy11600, vuy1180, vuy11600, vuy1180)

The remaining pairs can at least be oriented weakly.

new_primDivNatS0(vuy135, vuy136, Zero, Zero) → new_primDivNatS00(vuy135, vuy136)
new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Succ(vuy1380)) → new_primDivNatS0(vuy135, vuy136, vuy1370, vuy1380)
new_primDivNatS00(vuy135, vuy136) → new_primDivNatS(Succ(vuy135), Succ(vuy136), Succ(vuy136))
new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Zero) → new_primDivNatS(Succ(vuy135), Succ(vuy136), Succ(vuy136))

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂, x₃)) = x₁
POL(new_primDivNatS0(x₁, x₂, x₃, x₄)) = 1 + x₁
POL(new_primDivNatS00(x₁, x₂)) = 1 + x₁

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy135, vuy136, Zero, Zero) → new_primDivNatS00(vuy135, vuy136)
new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Succ(vuy1380)) → new_primDivNatS0(vuy135, vuy136, vuy1370, vuy1380)
new_primDivNatS00(vuy135, vuy136) → new_primDivNatS(Succ(vuy135), Succ(vuy136), Succ(vuy136))
new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Zero) → new_primDivNatS(Succ(vuy135), Succ(vuy136), Succ(vuy136))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Succ(vuy1380)) → new_primDivNatS0(vuy135, vuy136, vuy1370, vuy1380)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS0(vuy135, vuy136, Succ(vuy1370), Succ(vuy1380)) → new_primDivNatS0(vuy135, vuy136, vuy1370, vuy1380)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(vuy111, vuy112, Succ(vuy1130), Succ(vuy1140)) → new_primPlusNat(vuy111, vuy112, vuy1130, vuy1140)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(vuy111, vuy112, Succ(vuy1130), Succ(vuy1140)) → new_primPlusNat(vuy111, vuy112, vuy1130, vuy1140)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat0(Succ(vuy640), Succ(vuy650), vuy66) → new_primPlusNat0(vuy640, vuy650, vuy66)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat0(Succ(vuy640), Succ(vuy650), vuy66) → new_primPlusNat0(vuy640, vuy650, vuy66)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat1(vuy51, vuy52, Succ(vuy530), Succ(vuy540)) → new_primPlusNat1(vuy51, vuy52, vuy530, vuy540)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat1(vuy51, vuy52, Succ(vuy530), Succ(vuy540)) → new_primPlusNat1(vuy51, vuy52, vuy530, vuy540)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(vuy95, vuy96, Succ(vuy970), Succ(vuy980)) → new_primMinusNat(vuy95, vuy96, vuy970, vuy980)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(vuy95, vuy96, Succ(vuy970), Succ(vuy980)) → new_primMinusNat(vuy95, vuy96, vuy970, vuy980)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat0(Succ(vuy580), Succ(vuy590), vuy60) → new_primMinusNat0(vuy580, vuy590, vuy60)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat0(Succ(vuy580), Succ(vuy590), vuy60) → new_primMinusNat0(vuy580, vuy590, vuy60)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat1(vuy38, vuy39, Succ(vuy400), Succ(vuy410)) → new_primMinusNat1(vuy38, vuy39, vuy400, vuy410)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat1(vuy38, vuy39, Succ(vuy400), Succ(vuy410)) → new_primMinusNat1(vuy38, vuy39, vuy400, vuy410)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x

toEnum	zx	= toEnum11 zx
toEnum	yz	= toEnum9 yz
toEnum	yy	= toEnum7 yy